:: MMLQUERY semantic presentation

begin

definition
let X be set ;
mode List of X is Subset of X;
mode Operation of X is Relation of X;
end;

definition
let x, y, R be set ;
predx,y in R means :Def1: :: MMLQUERY:def 1
[x,y] in R;
end;

:: deftheorem Def1 defines in MMLQUERY:def_1_:_
 for x, y, R being set holds
( x,y in R iff [x,y] in R );

notation
let x, y, R be set ;
antonym x,y nin R for x,y in R;
end;


theorem Th9: :: MMLQUERY:1
for R1, R2 being Relation holds
( R1 c= R2 iff for z being set holds Im (R1,z) c= Im (R2,z) )
proof
let R1, R2 be Relation; ::_thesis: ( R1 c= R2 iff for z being set holds Im (R1,z) c= Im (R2,z) )
hereby  ::_thesis: ( ( for z being set holds Im (R1,z) c= Im (R2,z) ) implies R1 c= R2 )
assume Z1: R1 c= R2 ; ::_thesis: for z being set holds Im (R1,z) c= Im (R2,z)
let z be set ; ::_thesis: Im (R1,z) c= Im (R2,z)
thus  Im (R1,z) c= Im (R2,z) ::_thesis: verum
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in Im (R1,z) or s in Im (R2,z) )
assume  s in Im (R1,z) ; ::_thesis: s in Im (R2,z)
then consider v being set  such that
A1: ( [v,s] in R1 & v in {z} ) by RELAT_1:def_13;
thus  s in Im (R2,z) by Z1, A1, RELAT_1:def_13; ::_thesis: verum
end;
end;
assume Z2: for z being set holds Im (R1,z) c= Im (R2,z) ; ::_thesis: R1 c= R2
let a, b be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [a,b] in R1 or [a,b] in R2 )
assume  [a,b] in R1 ; ::_thesis: [a,b] in R2
then  ( b in Im (R1,a) & Im (R1,a) c= Im (R2,a) ) by Z2, RELAT_1:169;
hence  [a,b] in R2 by RELAT_1:169; ::_thesis: verum
end;

notation
let X be set ;
let O be Operation of X;
let x be Element of X;
synonym x . O for  Im (X,O);
end;

definition
let X be set ;
let O be Operation of X;
let x be Element of X;
:: original: .
redefine funcx . O ->  List of X;
coherence
 . x is List of X
proof
 . x = O .: {x} ;
hence  . x is Subset of X ; ::_thesis: verum
end;
end;

theorem Th0: :: MMLQUERY:2
for X being set
for x being Element of X
for O being Operation of X
for y being Element of X holds
( x,y in O iff y in x . O )
proof
let X be set ; ::_thesis: for x being Element of X
for O being Operation of X
for y being Element of X holds
( x,y in O iff y in x . O )
let x be Element of X; ::_thesis: for O being Operation of X
for y being Element of X holds
( x,y in O iff y in x . O )
let O be Operation of X; ::_thesis: for y being Element of X holds
( x,y in O iff y in x . O )
let y be Element of X; ::_thesis: ( x,y in O iff y in x . O )
 ( x,y in O iff [x,y] in O ) by Def1;
hence  ( x,y in O iff y in x . O ) by RELAT_1:169; ::_thesis: verum
end;

notation
let X be set ;
let O be Operation of X;
let L be List of X;
synonym L | O for X .: O;
end;

definition
let X be set ;
let O be Operation of X;
let L be List of X;
:: original: |
redefine funcL | O ->  List of X equals :: MMLQUERY:def 2
 union  {  (x . O) where x is Element of X : x in L  }  ;
coherence
 | L is List of X
proof
thus  O .: L is Subset of X ; ::_thesis: verum
end;
compatibility
 for b1 being List of X holds
( b1 = | L iff b1 = union  {  (x . O) where x is Element of X : x in L  }  )
proof
 union  {  (x . O) where x is Element of X : x in L  }  = | L
proof
thus  union  {  (x . O) where x is Element of X : x in L  }  c= | L :: according to XBOOLE_0:def_10 ::_thesis: | L c= union  {  (x . O) where x is Element of X : x in L  }
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union  {  (x . O) where x is Element of X : x in L  }  or z in | L )
assume  z in union  {  (x . O) where x is Element of X : x in L  }  ; ::_thesis: z in | L
then consider Y being set  such that
A1: ( z in Y & Y in  {  (x . O) where x is Element of X : x in L  }  ) by TARSKI:def_4;
consider x being Element of X such that
A2: ( Y = x . O & x in L ) by A1;
 [x,z] in O by A1, A2, RELAT_1:169;
hence  z in | L by A2, RELAT_1:def_13; ::_thesis: verum
end;
thus  | L c= union  {  (x . O) where x is Element of X : x in L  }  ::_thesis: verum
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in | L or z in union  {  (x . O) where x is Element of X : x in L  }  )
assume  z in | L ; ::_thesis: z in union  {  (x . O) where x is Element of X : x in L  }
then consider y being set  such that
A3: ( [y,z] in O & y in L ) by RELAT_1:def_13;
reconsider y = y as Element of X by A3;
 ( z in y . O & y . O in  {  (x . O) where x is Element of X : x in L  }  ) by A3, RELAT_1:169;
hence  z in union  {  (x . O) where x is Element of X : x in L  }  by TARSKI:def_4; ::_thesis: verum
end;
end;
hence  for b1 being List of X holds
( b1 = | L iff b1 = union  {  (x . O) where x is Element of X : x in L  }  ) ; ::_thesis: verum
end;
funcL \& O ->  List of X equals :: MMLQUERY:def 3
 meet  {  (x . O) where x is Element of X : x in L  }  ;
coherence
 meet  {  (x . O) where x is Element of X : x in L  }  is List of X
proof
 meet  {  (x . O) where x is Element of X : x in L  }  c= X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in meet  {  (x . O) where x is Element of X : x in L  }  or z in X )
assume A1: z in meet  {  (x . O) where x is Element of X : x in L  }  ; ::_thesis: z in X
then   {  (x . O) where x is Element of X : x in L  }  <> {} by SETFAM_1:def_1;
then consider Y being set  such that
A2: Y in  {  (x . O) where x is Element of X : x in L  }  by XBOOLE_0:def_1;
consider x being Element of X such that
A3: ( Y = x . O & x in L ) by A2;
 z in x . O by A1, A2, A3, SETFAM_1:def_1;
hence  z in X ; ::_thesis: verum
end;
hence  meet  {  (x . O) where x is Element of X : x in L  }  is List of X ; ::_thesis: verum
end;
funcL WHERE O ->  List of X equals :: MMLQUERY:def 4
 {  x where x is Element of X : ex y being Element of X st
( x,y in O & x in L )  }  ;
coherence
  {  x where x is Element of X : ex y being Element of X st
( x,y in O & x in L )  }  is List of X
proof
  {  x where x is Element of X : ex y being Element of X st
( x,y in O & x in L )  }  c= X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  x where x is Element of X : ex y being Element of X st
( x,y in O & x in L )  }  or z in X )
assume  z in  {  x where x is Element of X : ex y being Element of X st
( x,y in O & x in L )  }  ; ::_thesis: z in X
then consider x being Element of X such that
A1: ( z = x & ex y being Element of X st
( x,y in O & x in L ) ) ;
thus  z in X by A1; ::_thesis: verum
end;
hence   {  x where x is Element of X : ex y being Element of X st
( x,y in O & x in L )  }  is List of X ; ::_thesis: verum
end;
let O2 be Operation of X;
funcL WHEREeq (O,O2) ->  List of X equals :: MMLQUERY:def 5
 {  x where x is Element of X : ( card (x . O) = card (x . O2) & x in L )  }  ;
coherence
  {  x where x is Element of X : ( card (x . O) = card (x . O2) & x in L )  }  is List of X
proof
  {  x where x is Element of X : ( card (x . O) = card (x . O2) & x in L )  }  c= X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  x where x is Element of X : ( card (x . O) = card (x . O2) & x in L )  }  or z in X )
assume  z in  {  x where x is Element of X : ( card (x . O) = card (x . O2) & x in L )  }  ; ::_thesis: z in X
then  ex x being Element of X st
( z = x & card (x . O) = card (x . O2) & x in L ) ;
hence  z in X ; ::_thesis: verum
end;
hence   {  x where x is Element of X : ( card (x . O) = card (x . O2) & x in L )  }  is List of X ; ::_thesis: verum
end;
funcL WHEREle (O,O2) ->  List of X equals :: MMLQUERY:def 6
 {  x where x is Element of X : ( card (x . O) c= card (x . O2) & x in L )  }  ;
coherence
  {  x where x is Element of X : ( card (x . O) c= card (x . O2) & x in L )  }  is List of X
proof
  {  x where x is Element of X : ( card (x . O) c= card (x . O2) & x in L )  }  c= X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  x where x is Element of X : ( card (x . O) c= card (x . O2) & x in L )  }  or z in X )
assume  z in  {  x where x is Element of X : ( card (x . O) c= card (x . O2) & x in L )  }  ; ::_thesis: z in X
then  ex x being Element of X st
( z = x & card (x . O) c= card (x . O2) & x in L ) ;
hence  z in X ; ::_thesis: verum
end;
hence   {  x where x is Element of X : ( card (x . O) c= card (x . O2) & x in L )  }  is List of X ; ::_thesis: verum
end;
funcL WHEREge (O,O2) ->  List of X equals :: MMLQUERY:def 7
 {  x where x is Element of X : ( card (x . O2) c= card (x . O) & x in L )  }  ;
coherence
  {  x where x is Element of X : ( card (x . O2) c= card (x . O) & x in L )  }  is List of X
proof
  {  x where x is Element of X : ( card (x . O2) c= card (x . O) & x in L )  }  c= X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  x where x is Element of X : ( card (x . O2) c= card (x . O) & x in L )  }  or z in X )
assume  z in  {  x where x is Element of X : ( card (x . O2) c= card (x . O) & x in L )  }  ; ::_thesis: z in X
then  ex x being Element of X st
( z = x & card (x . O2) c= card (x . O) & x in L ) ;
hence  z in X ; ::_thesis: verum
end;
hence   {  x where x is Element of X : ( card (x . O2) c= card (x . O) & x in L )  }  is List of X ; ::_thesis: verum
end;
funcL WHERElt (O,O2) ->  List of X equals :: MMLQUERY:def 8
 {  x where x is Element of X : ( card (x . O) in card (x . O2) & x in L )  }  ;
coherence
  {  x where x is Element of X : ( card (x . O) in card (x . O2) & x in L )  }  is List of X
proof
  {  x where x is Element of X : ( card (x . O) in card (x . O2) & x in L )  }  c= X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  x where x is Element of X : ( card (x . O) in card (x . O2) & x in L )  }  or z in X )
assume  z in  {  x where x is Element of X : ( card (x . O) in card (x . O2) & x in L )  }  ; ::_thesis: z in X
then  ex x being Element of X st
( z = x & card (x . O) in card (x . O2) & x in L ) ;
hence  z in X ; ::_thesis: verum
end;
hence   {  x where x is Element of X : ( card (x . O) in card (x . O2) & x in L )  }  is List of X ; ::_thesis: verum
end;
funcL WHEREgt (O,O2) ->  List of X equals :: MMLQUERY:def 9
 {  x where x is Element of X : ( card (x . O2) in card (x . O) & x in L )  }  ;
coherence
  {  x where x is Element of X : ( card (x . O2) in card (x . O) & x in L )  }  is List of X
proof
  {  x where x is Element of X : ( card (x . O2) in card (x . O) & x in L )  }  c= X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  x where x is Element of X : ( card (x . O2) in card (x . O) & x in L )  }  or z in X )
assume  z in  {  x where x is Element of X : ( card (x . O2) in card (x . O) & x in L )  }  ; ::_thesis: z in X
then  ex x being Element of X st
( z = x & card (x . O2) in card (x . O) & x in L ) ;
hence  z in X ; ::_thesis: verum
end;
hence   {  x where x is Element of X : ( card (x . O2) in card (x . O) & x in L )  }  is List of X ; ::_thesis: verum
end;
end;

:: deftheorem  defines | MMLQUERY:def_2_:_
 for X being set
for O being Operation of X
for L being List of X holds L | O = union  {  (x . O) where x is Element of X : x in L  }  ;

:: deftheorem  defines \& MMLQUERY:def_3_:_
 for X being set
for O being Operation of X
for L being List of X holds L \& O = meet  {  (x . O) where x is Element of X : x in L  }  ;

:: deftheorem  defines WHERE MMLQUERY:def_4_:_
 for X being set
for O being Operation of X
for L being List of X holds L WHERE O =  {  x where x is Element of X : ex y being Element of X st
( x,y in O & x in L )  }  ;

:: deftheorem  defines WHEREeq MMLQUERY:def_5_:_
 for X being set
for O being Operation of X
for L being List of X
for O2 being Operation of X holds L WHEREeq (O,O2) =  {  x where x is Element of X : ( card (x . O) = card (x . O2) & x in L )  }  ;

:: deftheorem  defines WHEREle MMLQUERY:def_6_:_
 for X being set
for O being Operation of X
for L being List of X
for O2 being Operation of X holds L WHEREle (O,O2) =  {  x where x is Element of X : ( card (x . O) c= card (x . O2) & x in L )  }  ;

:: deftheorem  defines WHEREge MMLQUERY:def_7_:_
 for X being set
for O being Operation of X
for L being List of X
for O2 being Operation of X holds L WHEREge (O,O2) =  {  x where x is Element of X : ( card (x . O2) c= card (x . O) & x in L )  }  ;

:: deftheorem  defines WHERElt MMLQUERY:def_8_:_
 for X being set
for O being Operation of X
for L being List of X
for O2 being Operation of X holds L WHERElt (O,O2) =  {  x where x is Element of X : ( card (x . O) in card (x . O2) & x in L )  }  ;

:: deftheorem  defines WHEREgt MMLQUERY:def_9_:_
 for X being set
for O being Operation of X
for L being List of X
for O2 being Operation of X holds L WHEREgt (O,O2) =  {  x where x is Element of X : ( card (x . O2) in card (x . O) & x in L )  }  ;

definition
let X be set ;
let L be List of X;
let O be Operation of X;
let n be Nat;
funcL WHEREeq (O,n) ->  List of X equals :: MMLQUERY:def 10
 {  x where x is Element of X : ( card (x . O) = n & x in L )  }  ;
coherence
  {  x where x is Element of X : ( card (x . O) = n & x in L )  }  is List of X
proof
  {  x where x is Element of X : ( card (x . O) = n & x in L )  }  c= X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  x where x is Element of X : ( card (x . O) = n & x in L )  }  or z in X )
assume  z in  {  x where x is Element of X : ( card (x . O) = n & x in L )  }  ; ::_thesis: z in X
then  ex x being Element of X st
( z = x & card (x . O) = n & x in L ) ;
hence  z in X ; ::_thesis: verum
end;
hence   {  x where x is Element of X : ( card (x . O) = n & x in L )  }  is List of X ; ::_thesis: verum
end;
funcL WHEREle (O,n) ->  List of X equals :: MMLQUERY:def 11
 {  x where x is Element of X : ( card (x . O) c= n & x in L )  }  ;
coherence
  {  x where x is Element of X : ( card (x . O) c= n & x in L )  }  is List of X
proof
  {  x where x is Element of X : ( card (x . O) c= n & x in L )  }  c= X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  x where x is Element of X : ( card (x . O) c= n & x in L )  }  or z in X )
assume  z in  {  x where x is Element of X : ( card (x . O) c= n & x in L )  }  ; ::_thesis: z in X
then  ex x being Element of X st
( z = x & card (x . O) c= n & x in L ) ;
hence  z in X ; ::_thesis: verum
end;
hence   {  x where x is Element of X : ( card (x . O) c= n & x in L )  }  is List of X ; ::_thesis: verum
end;
funcL WHEREge (O,n) ->  List of X equals :: MMLQUERY:def 12
 {  x where x is Element of X : ( n c= card (x . O) & x in L )  }  ;
coherence
  {  x where x is Element of X : ( n c= card (x . O) & x in L )  }  is List of X
proof
  {  x where x is Element of X : ( n c= card (x . O) & x in L )  }  c= X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  x where x is Element of X : ( n c= card (x . O) & x in L )  }  or z in X )
assume  z in  {  x where x is Element of X : ( n c= card (x . O) & x in L )  }  ; ::_thesis: z in X
then  ex x being Element of X st
( z = x & n c= card (x . O) & x in L ) ;
hence  z in X ; ::_thesis: verum
end;
hence   {  x where x is Element of X : ( n c= card (x . O) & x in L )  }  is List of X ; ::_thesis: verum
end;
funcL WHERElt (O,n) ->  List of X equals :: MMLQUERY:def 13
 {  x where x is Element of X : ( card (x . O) in n & x in L )  }  ;
coherence
  {  x where x is Element of X : ( card (x . O) in n & x in L )  }  is List of X
proof
  {  x where x is Element of X : ( card (x . O) in n & x in L )  }  c= X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  x where x is Element of X : ( card (x . O) in n & x in L )  }  or z in X )
assume  z in  {  x where x is Element of X : ( card (x . O) in n & x in L )  }  ; ::_thesis: z in X
then  ex x being Element of X st
( z = x & card (x . O) in n & x in L ) ;
hence  z in X ; ::_thesis: verum
end;
hence   {  x where x is Element of X : ( card (x . O) in n & x in L )  }  is List of X ; ::_thesis: verum
end;
funcL WHEREgt (O,n) ->  List of X equals :: MMLQUERY:def 14
 {  x where x is Element of X : ( n in card (x . O) & x in L )  }  ;
coherence
  {  x where x is Element of X : ( n in card (x . O) & x in L )  }  is List of X
proof
  {  x where x is Element of X : ( n in card (x . O) & x in L )  }  c= X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  x where x is Element of X : ( n in card (x . O) & x in L )  }  or z in X )
assume  z in  {  x where x is Element of X : ( n in card (x . O) & x in L )  }  ; ::_thesis: z in X
then  ex x being Element of X st
( z = x & n in card (x . O) & x in L ) ;
hence  z in X ; ::_thesis: verum
end;
hence   {  x where x is Element of X : ( n in card (x . O) & x in L )  }  is List of X ; ::_thesis: verum
end;
end;

:: deftheorem  defines WHEREeq MMLQUERY:def_10_:_
 for X being set
for L being List of X
for O being Operation of X
for n being Nat holds L WHEREeq (O,n) =  {  x where x is Element of X : ( card (x . O) = n & x in L )  }  ;

:: deftheorem  defines WHEREle MMLQUERY:def_11_:_
 for X being set
for L being List of X
for O being Operation of X
for n being Nat holds L WHEREle (O,n) =  {  x where x is Element of X : ( card (x . O) c= n & x in L )  }  ;

:: deftheorem  defines WHEREge MMLQUERY:def_12_:_
 for X being set
for L being List of X
for O being Operation of X
for n being Nat holds L WHEREge (O,n) =  {  x where x is Element of X : ( n c= card (x . O) & x in L )  }  ;

:: deftheorem  defines WHERElt MMLQUERY:def_13_:_
 for X being set
for L being List of X
for O being Operation of X
for n being Nat holds L WHERElt (O,n) =  {  x where x is Element of X : ( card (x . O) in n & x in L )  }  ;

:: deftheorem  defines WHEREgt MMLQUERY:def_14_:_
 for X being set
for L being List of X
for O being Operation of X
for n being Nat holds L WHEREgt (O,n) =  {  x where x is Element of X : ( n in card (x . O) & x in L )  }  ;

theorem ThW: :: MMLQUERY:3
for X being set
for L being List of X
for x being Element of X
for O being Operation of X holds
( x in L WHERE O iff ( x in L & x . O <> {} ) )
proof
let X be set ; ::_thesis: for L being List of X
for x being Element of X
for O being Operation of X holds
( x in L WHERE O iff ( x in L & x . O <> {} ) )
let L be List of X; ::_thesis: for x being Element of X
for O being Operation of X holds
( x in L WHERE O iff ( x in L & x . O <> {} ) )
let x be Element of X; ::_thesis: for O being Operation of X holds
( x in L WHERE O iff ( x in L & x . O <> {} ) )
let O be Operation of X; ::_thesis: ( x in L WHERE O iff ( x in L & x . O <> {} ) )
hereby  ::_thesis: ( x in L & x . O <> {} implies x in L WHERE O )
assume  x in L WHERE O ; ::_thesis: ( x in L & x . O <> {} )
then consider y being Element of X such that
A1: ( x = y & ex a being Element of X st
( y,a in O & y in L ) ) ;
thus  ( x in L & x . O <> {} ) by A1, Th0; ::_thesis: verum
end;
assume A3: ( x in L & x . O <> {} ) ; ::_thesis: x in L WHERE O
set y = the Element of x . O;
 the Element of x . O in x . O by A3;
then reconsider y = the Element of x . O as Element of X ;
 x,y in O by A3, Th0;
hence  x in L WHERE O by A3; ::_thesis: verum
end;

theorem Th56: :: MMLQUERY:4
for X being set
for L being List of X
for O being Operation of X holds L WHERE O c= L
proof
let X be set ; ::_thesis: for L being List of X
for O being Operation of X holds L WHERE O c= L
let L be List of X; ::_thesis: for O being Operation of X holds L WHERE O c= L
let O be Operation of X; ::_thesis: L WHERE O c= L
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L WHERE O or z in L )
thus  ( not z in L WHERE O or z in L ) by ThW; ::_thesis: verum
end;

theorem :: MMLQUERY:5
for X being set
for L being List of X
for O being Operation of X st L c= dom O holds
L WHERE O = L
proof
let X be set ; ::_thesis: for L being List of X
for O being Operation of X st L c= dom O holds
L WHERE O = L
let L be List of X; ::_thesis: for O being Operation of X st L c= dom O holds
L WHERE O = L
let O be Operation of X; ::_thesis: ( L c= dom O implies L WHERE O = L )
assume A1: L c= dom O ; ::_thesis: L WHERE O = L
thus  L WHERE O c= L by Th56; :: according to XBOOLE_0:def_10 ::_thesis: L c= L WHERE O
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L or z in L WHERE O )
assume A2: z in L ; ::_thesis: z in L WHERE O
then reconsider z = z as Element of X ;
 z . O <> {} by A1, A2, RELAT_1:170;
hence  z in L WHERE O by A2, ThW; ::_thesis: verum
end;

theorem Th26: :: MMLQUERY:6
for X being set
for L1, L2 being List of X
for O being Operation of X
for n being Nat st n <> 0 & L1 c= L2 holds
L1 WHEREge (O,n) c= L2 WHERE O
proof
let X be set ; ::_thesis: for L1, L2 being List of X
for O being Operation of X
for n being Nat st n <> 0 & L1 c= L2 holds
L1 WHEREge (O,n) c= L2 WHERE O
let L1, L2 be List of X; ::_thesis: for O being Operation of X
for n being Nat st n <> 0 & L1 c= L2 holds
L1 WHEREge (O,n) c= L2 WHERE O
let O be Operation of X; ::_thesis: for n being Nat st n <> 0 & L1 c= L2 holds
L1 WHEREge (O,n) c= L2 WHERE O
let n be Nat; ::_thesis: ( n <> 0 & L1 c= L2 implies L1 WHEREge (O,n) c= L2 WHERE O )
assume A1: ( n <> 0 & L1 c= L2 ) ; ::_thesis: L1 WHEREge (O,n) c= L2 WHERE O
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L1 WHEREge (O,n) or z in L2 WHERE O )
assume  z in L1 WHEREge (O,n) ; ::_thesis: z in L2 WHERE O
then consider x being Element of X such that
A2: ( z = x & n c= card (x . O) & x in L1 ) ;
 x . O <> {} by A1, A2;
hence  z in L2 WHERE O by A1, A2, ThW; ::_thesis: verum
end;

theorem :: MMLQUERY:7
for X being set
for L being List of X
for O being Operation of X holds L WHEREge (O,1) = L WHERE O
proof
let X be set ; ::_thesis: for L being List of X
for O being Operation of X holds L WHEREge (O,1) = L WHERE O
let L be List of X; ::_thesis: for O being Operation of X holds L WHEREge (O,1) = L WHERE O
let O be Operation of X; ::_thesis: L WHEREge (O,1) = L WHERE O
thus  L WHEREge (O,1) c= L WHERE O by Th26; :: according to XBOOLE_0:def_10 ::_thesis: L WHERE O c= L WHEREge (O,1)
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L WHERE O or z in L WHEREge (O,1) )
assume A1: z in L WHERE O ; ::_thesis: z in L WHEREge (O,1)
then reconsider z = z as Element of X ;
A2: ( z . O <> {} & z in L ) by A1, ThW;
then  succ 0 c= card (z . O) by ORDINAL1:21, ORDINAL3:8;
hence  z in L WHEREge (O,1) by A2; ::_thesis: verum
end;

theorem Th27: :: MMLQUERY:8
for X being set
for L1, L2 being List of X
for O being Operation of X
for n being Nat st L1 c= L2 holds
L1 WHEREgt (O,n) c= L2 WHERE O
proof
let X be set ; ::_thesis: for L1, L2 being List of X
for O being Operation of X
for n being Nat st L1 c= L2 holds
L1 WHEREgt (O,n) c= L2 WHERE O
let L1, L2 be List of X; ::_thesis: for O being Operation of X
for n being Nat st L1 c= L2 holds
L1 WHEREgt (O,n) c= L2 WHERE O
let O be Operation of X; ::_thesis: for n being Nat st L1 c= L2 holds
L1 WHEREgt (O,n) c= L2 WHERE O
let n be Nat; ::_thesis: ( L1 c= L2 implies L1 WHEREgt (O,n) c= L2 WHERE O )
assume A1: L1 c= L2 ; ::_thesis: L1 WHEREgt (O,n) c= L2 WHERE O
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L1 WHEREgt (O,n) or z in L2 WHERE O )
assume  z in L1 WHEREgt (O,n) ; ::_thesis: z in L2 WHERE O
then consider x being Element of X such that
A2: ( z = x & n in card (x . O) & x in L1 ) ;
 x . O <> {} by A2;
hence  z in L2 WHERE O by A1, A2, ThW; ::_thesis: verum
end;

theorem :: MMLQUERY:9
for X being set
for L being List of X
for O being Operation of X holds L WHEREgt (O,0) = L WHERE O
proof
let X be set ; ::_thesis: for L being List of X
for O being Operation of X holds L WHEREgt (O,0) = L WHERE O
let L be List of X; ::_thesis: for O being Operation of X holds L WHEREgt (O,0) = L WHERE O
let O be Operation of X; ::_thesis: L WHEREgt (O,0) = L WHERE O
thus  L WHEREgt (O,0) c= L WHERE O by Th27; :: according to XBOOLE_0:def_10 ::_thesis: L WHERE O c= L WHEREgt (O,0)
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L WHERE O or z in L WHEREgt (O,0) )
assume A1: z in L WHERE O ; ::_thesis: z in L WHEREgt (O,0)
then reconsider z = z as Element of X ;
A2: ( z . O <> {} & z in L ) by A1, ThW;
then  0 in card (z . O) by ORDINAL3:8;
hence  z in L WHEREgt (O,0) by A2; ::_thesis: verum
end;

theorem :: MMLQUERY:10
for X being set
for L1, L2 being List of X
for O being Operation of X
for n being Nat st n <> 0 & L1 c= L2 holds
L1 WHEREeq (O,n) c= L2 WHERE O
proof
let X be set ; ::_thesis: for L1, L2 being List of X
for O being Operation of X
for n being Nat st n <> 0 & L1 c= L2 holds
L1 WHEREeq (O,n) c= L2 WHERE O
let L1, L2 be List of X; ::_thesis: for O being Operation of X
for n being Nat st n <> 0 & L1 c= L2 holds
L1 WHEREeq (O,n) c= L2 WHERE O
let O be Operation of X; ::_thesis: for n being Nat st n <> 0 & L1 c= L2 holds
L1 WHEREeq (O,n) c= L2 WHERE O
let n be Nat; ::_thesis: ( n <> 0 & L1 c= L2 implies L1 WHEREeq (O,n) c= L2 WHERE O )
assume A1: ( n <> 0 & L1 c= L2 ) ; ::_thesis: L1 WHEREeq (O,n) c= L2 WHERE O
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L1 WHEREeq (O,n) or z in L2 WHERE O )
assume  z in L1 WHEREeq (O,n) ; ::_thesis: z in L2 WHERE O
then consider x being Element of X such that
A2: ( z = x & card (x . O) = n & x in L1 ) ;
 x . O <> {} by A1, A2;
hence  z in L2 WHERE O by A1, A2, ThW; ::_thesis: verum
end;

theorem :: MMLQUERY:11
for X being set
for L being List of X
for O being Operation of X
for n being Nat holds L WHEREge (O,(n + 1)) = L WHEREgt (O,n)
proof
let X be set ; ::_thesis: for L being List of X
for O being Operation of X
for n being Nat holds L WHEREge (O,(n + 1)) = L WHEREgt (O,n)
let L be List of X; ::_thesis: for O being Operation of X
for n being Nat holds L WHEREge (O,(n + 1)) = L WHEREgt (O,n)
let O be Operation of X; ::_thesis: for n being Nat holds L WHEREge (O,(n + 1)) = L WHEREgt (O,n)
let n be Nat; ::_thesis: L WHEREge (O,(n + 1)) = L WHEREgt (O,n)
thus  L WHEREge (O,(n + 1)) c= L WHEREgt (O,n) :: according to XBOOLE_0:def_10 ::_thesis: L WHEREgt (O,n) c= L WHEREge (O,(n + 1))
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L WHEREge (O,(n + 1)) or z in L WHEREgt (O,n) )
assume  z in L WHEREge (O,(n + 1)) ; ::_thesis: z in L WHEREgt (O,n)
then consider x being Element of X such that
A2: ( z = x & n + 1 c= card (x . O) & x in L ) ;
 n + 1 = succ n by NAT_1:38;
then  n in card (x . O) by A2, ORDINAL1:21;
hence  z in L WHEREgt (O,n) by A2; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L WHEREgt (O,n) or z in L WHEREge (O,(n + 1)) )
assume  z in L WHEREgt (O,n) ; ::_thesis: z in L WHEREge (O,(n + 1))
then consider x being Element of X such that
A2: ( z = x & n in card (x . O) & x in L ) ;
 n + 1 = succ n by NAT_1:38;
then  n + 1 c= card (x . O) by A2, ORDINAL1:21;
hence  z in L WHEREge (O,(n + 1)) by A2; ::_thesis: verum
end;

theorem :: MMLQUERY:12
for X being set
for L being List of X
for O being Operation of X
for n being Nat holds L WHEREle (O,n) = L WHERElt (O,(n + 1))
proof
let X be set ; ::_thesis: for L being List of X
for O being Operation of X
for n being Nat holds L WHEREle (O,n) = L WHERElt (O,(n + 1))
let L be List of X; ::_thesis: for O being Operation of X
for n being Nat holds L WHEREle (O,n) = L WHERElt (O,(n + 1))
let O be Operation of X; ::_thesis: for n being Nat holds L WHEREle (O,n) = L WHERElt (O,(n + 1))
let n be Nat; ::_thesis: L WHEREle (O,n) = L WHERElt (O,(n + 1))
thus  L WHEREle (O,n) c= L WHERElt (O,(n + 1)) :: according to XBOOLE_0:def_10 ::_thesis: L WHERElt (O,(n + 1)) c= L WHEREle (O,n)
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L WHEREle (O,n) or z in L WHERElt (O,(n + 1)) )
assume  z in L WHEREle (O,n) ; ::_thesis: z in L WHERElt (O,(n + 1))
then consider x being Element of X such that
A2: ( z = x & card (x . O) c= n & x in L ) ;
 n + 1 = succ n by NAT_1:38;
then  card (x . O) in n + 1 by A2, ORDINAL1:22;
hence  z in L WHERElt (O,(n + 1)) by A2; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L WHERElt (O,(n + 1)) or z in L WHEREle (O,n) )
assume  z in L WHERElt (O,(n + 1)) ; ::_thesis: z in L WHEREle (O,n)
then consider x being Element of X such that
A2: ( z = x & card (x . O) in n + 1 & x in L ) ;
 n + 1 = succ n by NAT_1:38;
then  card (x . O) c= n by A2, ORDINAL1:22;
hence  z in L WHEREle (O,n) by A2; ::_thesis: verum
end;

theorem :: MMLQUERY:13
for X being set
for L1, L2 being List of X
for O1, O2 being Operation of X
for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds
L1 WHEREge (O1,m) c= L2 WHEREge (O2,n)
proof
let X be set ; ::_thesis: for L1, L2 being List of X
for O1, O2 being Operation of X
for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds
L1 WHEREge (O1,m) c= L2 WHEREge (O2,n)
let L1, L2 be List of X; ::_thesis: for O1, O2 being Operation of X
for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds
L1 WHEREge (O1,m) c= L2 WHEREge (O2,n)
let O1, O2 be Operation of X; ::_thesis: for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds
L1 WHEREge (O1,m) c= L2 WHEREge (O2,n)
let n, m be Nat; ::_thesis: ( n <= m & L1 c= L2 & O1 c= O2 implies L1 WHEREge (O1,m) c= L2 WHEREge (O2,n) )
assume A1: ( n <= m & L1 c= L2 & O1 c= O2 ) ; ::_thesis: L1 WHEREge (O1,m) c= L2 WHEREge (O2,n)
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L1 WHEREge (O1,m) or z in L2 WHEREge (O2,n) )
assume  z in L1 WHEREge (O1,m) ; ::_thesis: z in L2 WHEREge (O2,n)
then consider x being Element of X such that
A2: ( z = x & m c= card (x . O1) & x in L1 ) ;
 ( n c= m & x . O1 c= x . O2 ) by A1, Th9, NAT_1:39;
then  ( n c= card (x . O1) & card (x . O1) c= card (x . O2) ) by A2, CARD_1:11, XBOOLE_1:1;
then  n c= card (x . O2) by XBOOLE_1:1;
hence  z in L2 WHEREge (O2,n) by A1, A2; ::_thesis: verum
end;

theorem :: MMLQUERY:14
for X being set
for L1, L2 being List of X
for O1, O2 being Operation of X
for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds
L1 WHEREgt (O1,m) c= L2 WHEREgt (O2,n)
proof
let X be set ; ::_thesis: for L1, L2 being List of X
for O1, O2 being Operation of X
for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds
L1 WHEREgt (O1,m) c= L2 WHEREgt (O2,n)
let L1, L2 be List of X; ::_thesis: for O1, O2 being Operation of X
for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds
L1 WHEREgt (O1,m) c= L2 WHEREgt (O2,n)
let O1, O2 be Operation of X; ::_thesis: for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds
L1 WHEREgt (O1,m) c= L2 WHEREgt (O2,n)
let n, m be Nat; ::_thesis: ( n <= m & L1 c= L2 & O1 c= O2 implies L1 WHEREgt (O1,m) c= L2 WHEREgt (O2,n) )
assume A1: ( n <= m & L1 c= L2 & O1 c= O2 ) ; ::_thesis: L1 WHEREgt (O1,m) c= L2 WHEREgt (O2,n)
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L1 WHEREgt (O1,m) or z in L2 WHEREgt (O2,n) )
assume  z in L1 WHEREgt (O1,m) ; ::_thesis: z in L2 WHEREgt (O2,n)
then consider x being Element of X such that
A2: ( z = x & m in card (x . O1) & x in L1 ) ;
 ( n c= m & card (x . O1) c= card (x . O2) ) by A1, CARD_1:11, NAT_1:39, Th9;
then  n in card (x . O2) by A2, ORDINAL1:12;
hence  z in L2 WHEREgt (O2,n) by A1, A2; ::_thesis: verum
end;

theorem :: MMLQUERY:15
for X being set
for L1, L2 being List of X
for O1, O2 being Operation of X
for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds
L1 WHEREle (O2,n) c= L2 WHEREle (O1,m)
proof
let X be set ; ::_thesis: for L1, L2 being List of X
for O1, O2 being Operation of X
for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds
L1 WHEREle (O2,n) c= L2 WHEREle (O1,m)
let L1, L2 be List of X; ::_thesis: for O1, O2 being Operation of X
for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds
L1 WHEREle (O2,n) c= L2 WHEREle (O1,m)
let O1, O2 be Operation of X; ::_thesis: for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds
L1 WHEREle (O2,n) c= L2 WHEREle (O1,m)
let n, m be Nat; ::_thesis: ( n <= m & L1 c= L2 & O1 c= O2 implies L1 WHEREle (O2,n) c= L2 WHEREle (O1,m) )
assume A1: ( n <= m & L1 c= L2 & O1 c= O2 ) ; ::_thesis: L1 WHEREle (O2,n) c= L2 WHEREle (O1,m)
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L1 WHEREle (O2,n) or z in L2 WHEREle (O1,m) )
assume  z in L1 WHEREle (O2,n) ; ::_thesis: z in L2 WHEREle (O1,m)
then consider x being Element of X such that
A2: ( z = x & card (x . O2) c= n & x in L1 ) ;
 ( n c= m & x . O1 c= x . O2 ) by A1, Th9, NAT_1:39;
then  ( card (x . O1) c= card (x . O2) & card (x . O2) c= m ) by A2, CARD_1:11, XBOOLE_1:1;
then  card (x . O1) c= m by XBOOLE_1:1;
hence  z in L2 WHEREle (O1,m) by A1, A2; ::_thesis: verum
end;

theorem :: MMLQUERY:16
for X being set
for L1, L2 being List of X
for O1, O2 being Operation of X
for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds
L1 WHERElt (O2,n) c= L2 WHERElt (O1,m)
proof
let X be set ; ::_thesis: for L1, L2 being List of X
for O1, O2 being Operation of X
for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds
L1 WHERElt (O2,n) c= L2 WHERElt (O1,m)
let L1, L2 be List of X; ::_thesis: for O1, O2 being Operation of X
for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds
L1 WHERElt (O2,n) c= L2 WHERElt (O1,m)
let O1, O2 be Operation of X; ::_thesis: for n, m being Nat st n <= m & L1 c= L2 & O1 c= O2 holds
L1 WHERElt (O2,n) c= L2 WHERElt (O1,m)
let n, m be Nat; ::_thesis: ( n <= m & L1 c= L2 & O1 c= O2 implies L1 WHERElt (O2,n) c= L2 WHERElt (O1,m) )
assume A1: ( n <= m & L1 c= L2 & O1 c= O2 ) ; ::_thesis: L1 WHERElt (O2,n) c= L2 WHERElt (O1,m)
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L1 WHERElt (O2,n) or z in L2 WHERElt (O1,m) )
assume  z in L1 WHERElt (O2,n) ; ::_thesis: z in L2 WHERElt (O1,m)
then consider x being Element of X such that
A2: ( z = x & card (x . O2) in n & x in L1 ) ;
 ( n c= m & card (x . O1) c= card (x . O2) ) by A1, CARD_1:11, NAT_1:39, Th9;
then  card (x . O1) in m by A2, ORDINAL1:12;
hence  z in L2 WHERElt (O1,m) by A1, A2; ::_thesis: verum
end;

theorem :: MMLQUERY:17
for X being set
for L1, L2 being List of X
for O1, O2, O, O3 being Operation of X st O1 c= O2 & L1 c= L2 & O c= O3 holds
L1 WHEREge (O,O2) c= L2 WHEREge (O3,O1)
proof
let X be set ; ::_thesis: for L1, L2 being List of X
for O1, O2, O, O3 being Operation of X st O1 c= O2 & L1 c= L2 & O c= O3 holds
L1 WHEREge (O,O2) c= L2 WHEREge (O3,O1)
let L1, L2 be List of X; ::_thesis: for O1, O2, O, O3 being Operation of X st O1 c= O2 & L1 c= L2 & O c= O3 holds
L1 WHEREge (O,O2) c= L2 WHEREge (O3,O1)
let O1, O2, O, O3 be Operation of X; ::_thesis: ( O1 c= O2 & L1 c= L2 & O c= O3 implies L1 WHEREge (O,O2) c= L2 WHEREge (O3,O1) )
assume Z0: ( O1 c= O2 & L1 c= L2 & O c= O3 ) ; ::_thesis: L1 WHEREge (O,O2) c= L2 WHEREge (O3,O1)
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L1 WHEREge (O,O2) or z in L2 WHEREge (O3,O1) )
assume  z in L1 WHEREge (O,O2) ; ::_thesis: z in L2 WHEREge (O3,O1)
then consider x being Element of X such that
A1: ( z = x & card (x . O2) c= card (x . O) & x in L1 ) ;
A2: ( card (x . O1) c= card (x . O2) & card (x . O) c= card (x . O3) ) by Z0, Th9, CARD_1:11;
then  card (x . O1) c= card (x . O) by A1, XBOOLE_1:1;
then  card (x . O1) c= card (x . O3) by A2, XBOOLE_1:1;
hence  z in L2 WHEREge (O3,O1) by A1, Z0; ::_thesis: verum
end;

theorem :: MMLQUERY:18
for X being set
for L1, L2 being List of X
for O1, O2, O, O3 being Operation of X st O1 c= O2 & L1 c= L2 & O c= O3 holds
L1 WHEREgt (O,O2) c= L2 WHEREgt (O3,O1)
proof
let X be set ; ::_thesis: for L1, L2 being List of X
for O1, O2, O, O3 being Operation of X st O1 c= O2 & L1 c= L2 & O c= O3 holds
L1 WHEREgt (O,O2) c= L2 WHEREgt (O3,O1)
let L1, L2 be List of X; ::_thesis: for O1, O2, O, O3 being Operation of X st O1 c= O2 & L1 c= L2 & O c= O3 holds
L1 WHEREgt (O,O2) c= L2 WHEREgt (O3,O1)
let O1, O2, O, O3 be Operation of X; ::_thesis: ( O1 c= O2 & L1 c= L2 & O c= O3 implies L1 WHEREgt (O,O2) c= L2 WHEREgt (O3,O1) )
assume Z0: ( O1 c= O2 & L1 c= L2 & O c= O3 ) ; ::_thesis: L1 WHEREgt (O,O2) c= L2 WHEREgt (O3,O1)
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L1 WHEREgt (O,O2) or z in L2 WHEREgt (O3,O1) )
assume  z in L1 WHEREgt (O,O2) ; ::_thesis: z in L2 WHEREgt (O3,O1)
then consider x being Element of X such that
A1: ( z = x & card (x . O2) in card (x . O) & x in L1 ) ;
 ( x . O1 c= x . O2 & x . O c= x . O3 ) by Z0, Th9;
then  ( card (x . O1) in card (x . O) & card (x . O) c= card (x . O3) ) by A1, CARD_1:11, ORDINAL1:12;
hence  z in L2 WHEREgt (O3,O1) by A1, Z0; ::_thesis: verum
end;

theorem :: MMLQUERY:19
for X being set
for L1, L2 being List of X
for O1, O2, O, O3 being Operation of X st O1 c= O2 & L1 c= L2 & O c= O3 holds
L1 WHEREle (O3,O1) c= L2 WHEREle (O,O2)
proof
let X be set ; ::_thesis: for L1, L2 being List of X
for O1, O2, O, O3 being Operation of X st O1 c= O2 & L1 c= L2 & O c= O3 holds
L1 WHEREle (O3,O1) c= L2 WHEREle (O,O2)
let L1, L2 be List of X; ::_thesis: for O1, O2, O, O3 being Operation of X st O1 c= O2 & L1 c= L2 & O c= O3 holds
L1 WHEREle (O3,O1) c= L2 WHEREle (O,O2)
let O1, O2, O, O3 be Operation of X; ::_thesis: ( O1 c= O2 & L1 c= L2 & O c= O3 implies L1 WHEREle (O3,O1) c= L2 WHEREle (O,O2) )
assume Z0: ( O1 c= O2 & L1 c= L2 & O c= O3 ) ; ::_thesis: L1 WHEREle (O3,O1) c= L2 WHEREle (O,O2)
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L1 WHEREle (O3,O1) or z in L2 WHEREle (O,O2) )
assume  z in L1 WHEREle (O3,O1) ; ::_thesis: z in L2 WHEREle (O,O2)
then consider x being Element of X such that
A1: ( z = x & card (x . O3) c= card (x . O1) & x in L1 ) ;
A2: ( card (x . O1) c= card (x . O2) & card (x . O) c= card (x . O3) ) by Z0, Th9, CARD_1:11;
then  card (x . O3) c= card (x . O2) by A1, XBOOLE_1:1;
then  card (x . O) c= card (x . O2) by A2, XBOOLE_1:1;
hence  z in L2 WHEREle (O,O2) by A1, Z0; ::_thesis: verum
end;

theorem :: MMLQUERY:20
for X being set
for L1, L2 being List of X
for O1, O2, O, O3 being Operation of X st O1 c= O2 & L1 c= L2 & O c= O3 holds
L1 WHERElt (O3,O1) c= L2 WHERElt (O,O2)
proof
let X be set ; ::_thesis: for L1, L2 being List of X
for O1, O2, O, O3 being Operation of X st O1 c= O2 & L1 c= L2 & O c= O3 holds
L1 WHERElt (O3,O1) c= L2 WHERElt (O,O2)
let L1, L2 be List of X; ::_thesis: for O1, O2, O, O3 being Operation of X st O1 c= O2 & L1 c= L2 & O c= O3 holds
L1 WHERElt (O3,O1) c= L2 WHERElt (O,O2)
let O1, O2, O, O3 be Operation of X; ::_thesis: ( O1 c= O2 & L1 c= L2 & O c= O3 implies L1 WHERElt (O3,O1) c= L2 WHERElt (O,O2) )
assume Z0: ( O1 c= O2 & L1 c= L2 & O c= O3 ) ; ::_thesis: L1 WHERElt (O3,O1) c= L2 WHERElt (O,O2)
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L1 WHERElt (O3,O1) or z in L2 WHERElt (O,O2) )
assume  z in L1 WHERElt (O3,O1) ; ::_thesis: z in L2 WHERElt (O,O2)
then consider x being Element of X such that
A1: ( z = x & card (x . O3) in card (x . O1) & x in L1 ) ;
 ( card (x . O1) c= card (x . O2) & card (x . O) c= card (x . O3) ) by Z0, Th9, CARD_1:11;
then  card (x . O) in card (x . O2) by A1, ORDINAL1:12;
hence  z in L2 WHERElt (O,O2) by A1, Z0; ::_thesis: verum
end;

theorem :: MMLQUERY:21
for X being set
for L being List of X
for O, O1 being Operation of X holds L WHEREgt (O,O1) c= L WHERE O
proof
let X be set ; ::_thesis: for L being List of X
for O, O1 being Operation of X holds L WHEREgt (O,O1) c= L WHERE O
let L be List of X; ::_thesis: for O, O1 being Operation of X holds L WHEREgt (O,O1) c= L WHERE O
let O, O1 be Operation of X; ::_thesis: L WHEREgt (O,O1) c= L WHERE O
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L WHEREgt (O,O1) or z in L WHERE O )
assume  z in L WHEREgt (O,O1) ; ::_thesis: z in L WHERE O
then consider x being Element of X such that
A2: ( z = x & card (x . O1) in card (x . O) & x in L ) ;
 x . O <> {} by A2;
hence  z in L WHERE O by A2, ThW; ::_thesis: verum
end;

theorem :: MMLQUERY:22
for X being set
for L1, L2 being List of X
for O1, O2 being Operation of X st O1 c= O2 & L1 c= L2 holds
L1 WHERE O1 c= L2 WHERE O2
proof
let X be set ; ::_thesis: for L1, L2 being List of X
for O1, O2 being Operation of X st O1 c= O2 & L1 c= L2 holds
L1 WHERE O1 c= L2 WHERE O2
let L1, L2 be List of X; ::_thesis: for O1, O2 being Operation of X st O1 c= O2 & L1 c= L2 holds
L1 WHERE O1 c= L2 WHERE O2
let O1, O2 be Operation of X; ::_thesis: ( O1 c= O2 & L1 c= L2 implies L1 WHERE O1 c= L2 WHERE O2 )
assume A1: ( O1 c= O2 & L1 c= L2 ) ; ::_thesis: L1 WHERE O1 c= L2 WHERE O2
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L1 WHERE O1 or z in L2 WHERE O2 )
assume A2: z in L1 WHERE O1 ; ::_thesis: z in L2 WHERE O2
then reconsider z = z as Element of X ;
A3: ( z . O1 <> {} & z in L1 ) by A2, ThW;
 z . O1 c= z . O2 by A1, Th9;
then  z . O2 <> {} by A3;
hence  z in L2 WHERE O2 by A1, A3, ThW; ::_thesis: verum
end;

theorem Th1: :: MMLQUERY:23
for X being set
for L being List of X
for O being Operation of X
for a being Element of X holds
( a in L | O iff ex b being Element of X st
( a in b . O & b in L ) )
proof
let X be set ; ::_thesis: for L being List of X
for O being Operation of X
for a being Element of X holds
( a in L | O iff ex b being Element of X st
( a in b . O & b in L ) )
let L be List of X; ::_thesis: for O being Operation of X
for a being Element of X holds
( a in L | O iff ex b being Element of X st
( a in b . O & b in L ) )
let O be Operation of X; ::_thesis: for a being Element of X holds
( a in L | O iff ex b being Element of X st
( a in b . O & b in L ) )
let a be Element of X; ::_thesis: ( a in L | O iff ex b being Element of X st
( a in b . O & b in L ) )
hereby  ::_thesis: ( ex b being Element of X st
( a in b . O & b in L ) implies a in L | O )
assume  a in L | O ; ::_thesis: ex b being Element of X st
( a in b . O & b in L )
then consider b being set  such that
A1: ( [b,a] in O & b in L ) by RELAT_1:def_13;
reconsider b = b as Element of X by A1;
take b = b; ::_thesis: ( a in b . O & b in L )
thus  a in b . O by A1, RELAT_1:169; ::_thesis: b in L
thus  b in L by A1; ::_thesis: verum
end;
given b being Element of X such that A2: ( a in b . O & b in L ) ; ::_thesis: a in L | O
 [b,a] in O by A2, RELAT_1:169;
hence  a in L | O by A2, RELAT_1:def_13; ::_thesis: verum
end;

notation
let X be set ;
let A, B be List of X;
synonym A AND B for X /\ A;
synonym A OR B for X \/ A;
synonym A BUTNOT B for X \ A;
end;

definition
let X be set ;
let A, B be List of X;
:: original: AND
redefine funcA AND B ->  List of X;
coherence
 B AND is List of X
proof
 A /\ B is Subset of X ;
hence  B AND is List of X ; ::_thesis: verum
end;
:: original: OR
redefine funcA OR B ->  List of X;
coherence
 B OR is List of X
proof
 A \/ B is Subset of X ;
hence  B OR is List of X ; ::_thesis: verum
end;
:: original: BUTNOT
redefine funcA BUTNOT B ->  List of X;
coherence
 B BUTNOT is List of X
proof
 A \ B is Subset of X ;
hence  B BUTNOT is List of X ; ::_thesis: verum
end;
end;

theorem Th17: :: MMLQUERY:24
for X being set
for L1, L2 being List of X
for O being Operation of X st L1 <> {} & L2 <> {} holds
(L1 OR L2) \& O = (L1 \& O) AND (L2 \& O)
proof
let X be set ; ::_thesis: for L1, L2 being List of X
for O being Operation of X st L1 <> {} & L2 <> {} holds
(L1 OR L2) \& O = (L1 \& O) AND (L2 \& O)
let L1, L2 be List of X; ::_thesis: for O being Operation of X st L1 <> {} & L2 <> {} holds
(L1 OR L2) \& O = (L1 \& O) AND (L2 \& O)
let O be Operation of X; ::_thesis: ( L1 <> {} & L2 <> {} implies (L1 OR L2) \& O = (L1 \& O) AND (L2 \& O) )
assume A0: ( L1 <> {} & L2 <> {} ) ; ::_thesis: (L1 OR L2) \& O = (L1 \& O) AND (L2 \& O)
thus  (L1 OR L2) \& O c= (L1 \& O) AND (L2 \& O) :: according to XBOOLE_0:def_10 ::_thesis: (L1 \& O) AND (L2 \& O) c= (L1 OR L2) \& O
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in (L1 OR L2) \& O or z in (L1 \& O) AND (L2 \& O) )
assume A1: z in (L1 OR L2) \& O ; ::_thesis: z in (L1 \& O) AND (L2 \& O)
now__::_thesis:_(__{__(x_._O)_where_x_is_Element_of_X_:_x_in_L1__}__<>_{}_&_(_for_Y_being_set_st_Y_in__{__(x_._O)_where_x_is_Element_of_X_:_x_in_L1__}__holds_
z_in_Y_)_)
set c = the Element of L1;
 the Element of L1 in L1 by A0;
then reconsider c = the Element of L1 as Element of X ;
 c . O in  {  (x . O) where x is Element of X : x in L1  }  by A0;
hence   {  (x . O) where x is Element of X : x in L1  }  <> {} ; ::_thesis: for Y being set st Y in  {  (x . O) where x is Element of X : x in L1  }  holds
z in Y
let Y be set ; ::_thesis: ( Y in  {  (x . O) where x is Element of X : x in L1  }  implies z in Y )
assume  Y in  {  (x . O) where x is Element of X : x in L1  }  ; ::_thesis: z in Y
then consider x being Element of X such that
A3: ( Y = x . O & x in L1 ) ;
 x in L1 OR L2 by A3, XBOOLE_0:def_3;
then  Y in  {  (a . O) where a is Element of X : a in L1 OR L2  }  by A3;
hence  z in Y by A1, SETFAM_1:def_1; ::_thesis: verum
end;
then A4: z in L1 \& O by SETFAM_1:def_1;
now__::_thesis:_(__{__(x_._O)_where_x_is_Element_of_X_:_x_in_L2__}__<>_{}_&_(_for_Y_being_set_st_Y_in__{__(x_._O)_where_x_is_Element_of_X_:_x_in_L2__}__holds_
z_in_Y_)_)
set c = the Element of L2;
 the Element of L2 in L2 by A0;
then reconsider c = the Element of L2 as Element of X ;
 c . O in  {  (x . O) where x is Element of X : x in L2  }  by A0;
hence   {  (x . O) where x is Element of X : x in L2  }  <> {} ; ::_thesis: for Y being set st Y in  {  (x . O) where x is Element of X : x in L2  }  holds
z in Y
let Y be set ; ::_thesis: ( Y in  {  (x . O) where x is Element of X : x in L2  }  implies z in Y )
assume  Y in  {  (x . O) where x is Element of X : x in L2  }  ; ::_thesis: z in Y
then consider x being Element of X such that
A3: ( Y = x . O & x in L2 ) ;
 x in L1 OR L2 by A3, XBOOLE_0:def_3;
then  Y in  {  (a . O) where a is Element of X : a in L1 OR L2  }  by A3;
hence  z in Y by A1, SETFAM_1:def_1; ::_thesis: verum
end;
then  z in L2 \& O by SETFAM_1:def_1;
hence  z in (L1 \& O) AND (L2 \& O) by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in (L1 \& O) AND (L2 \& O) or z in (L1 OR L2) \& O )
assume  z in (L1 \& O) AND (L2 \& O) ; ::_thesis: z in (L1 OR L2) \& O
then A5: ( z in L1 \& O & z in L2 \& O ) by XBOOLE_0:def_4;
now__::_thesis:_(__{__(x_._O)_where_x_is_Element_of_X_:_x_in_L1_OR_L2__}__<>_{}_&_(_for_Y_being_set_st_Y_in__{__(x_._O)_where_x_is_Element_of_X_:_x_in_L1_OR_L2__}__holds_
z_in_Y_)_)
set c = the Element of L2;
 the Element of L2 in L2 by A0;
then reconsider c = the Element of L2 as Element of X ;
 c in L1 OR L2 by A0, XBOOLE_0:def_3;
then  c . O in  {  (x . O) where x is Element of X : x in L1 OR L2  }  ;
hence   {  (x . O) where x is Element of X : x in L1 OR L2  }  <> {} ; ::_thesis: for Y being set st Y in  {  (x . O) where x is Element of X : x in L1 OR L2  }  holds
z in Y
let Y be set ; ::_thesis: ( Y in  {  (x . O) where x is Element of X : x in L1 OR L2  }  implies z in Y )
assume  Y in  {  (x . O) where x is Element of X : x in L1 OR L2  }  ; ::_thesis: z in Y
then consider x being Element of X such that
A3: ( Y = x . O & x in L1 OR L2 ) ;
 ( x in L1 or x in L2 ) by A3, XBOOLE_0:def_3;
then  ( Y in  {  (a . O) where a is Element of X : a in L1  }  or Y in  {  (b . O) where b is Element of X : b in L2  }  ) by A3;
hence  z in Y by A5, SETFAM_1:def_1; ::_thesis: verum
end;
hence  z in (L1 OR L2) \& O by SETFAM_1:def_1; ::_thesis: verum
end;

theorem :: MMLQUERY:25
for X being set
for L1, L2 being List of X
for O1, O2 being Operation of X st L1 c= L2 & O1 c= O2 holds
L1 | O1 c= L2 | O2
proof
let X be set ; ::_thesis: for L1, L2 being List of X
for O1, O2 being Operation of X st L1 c= L2 & O1 c= O2 holds
L1 | O1 c= L2 | O2
let L1, L2 be List of X; ::_thesis: for O1, O2 being Operation of X st L1 c= L2 & O1 c= O2 holds
L1 | O1 c= L2 | O2
let O1, O2 be Operation of X; ::_thesis: ( L1 c= L2 & O1 c= O2 implies L1 | O1 c= L2 | O2 )
assume  ( L1 c= L2 & O1 c= O2 ) ; ::_thesis: L1 | O1 c= L2 | O2
then  ( L1 | O1 c= L2 | O1 & L2 | O1 c= L2 | O2 ) by RELAT_1:123, RELAT_1:124;
hence  L1 | O1 c= L2 | O2 by XBOOLE_1:1; ::_thesis: verum
end;

theorem Th81: :: MMLQUERY:26
for X being set
for L being List of X
for O1, O2 being Operation of X st O1 c= O2 holds
L \& O1 c= L \& O2
proof
let X be set ; ::_thesis: for L being List of X
for O1, O2 being Operation of X st O1 c= O2 holds
L \& O1 c= L \& O2
let L be List of X; ::_thesis: for O1, O2 being Operation of X st O1 c= O2 holds
L \& O1 c= L \& O2
let O1, O2 be Operation of X; ::_thesis: ( O1 c= O2 implies L \& O1 c= L \& O2 )
assume A1: O1 c= O2 ; ::_thesis: L \& O1 c= L \& O2
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L \& O1 or z in L \& O2 )
assume A2: z in L \& O1 ; ::_thesis: z in L \& O2
then   {  (x . O1) where x is Element of X : x in L  }  <> {} by SETFAM_1:def_1;
then consider Y being set  such that
A3: Y in  {  (x . O1) where x is Element of X : x in L  }  by XBOOLE_0:def_1;
consider y being Element of X such that
A4: ( Y = y . O1 & y in L ) by A3;
A5: y . O2 in  {  (x . O2) where x is Element of X : x in L  }  by A4;
now__::_thesis:_for_Y_being_set_st_Y_in__{__(x_._O2)_where_x_is_Element_of_X_:_x_in_L__}__holds_
z_in_Y
let Y be set ; ::_thesis: ( Y in  {  (x . O2) where x is Element of X : x in L  }  implies z in Y )
assume  Y in  {  (x . O2) where x is Element of X : x in L  }  ; ::_thesis: z in Y
then consider a being Element of X such that
A6: ( Y = a . O2 & a in L ) ;
 a . O1 in  {  (x . O1) where x is Element of X : x in L  }  by A6;
then  ( z in a . O1 & a . O1 c= Y ) by A1, A2, A6, Th9, SETFAM_1:def_1;
hence  z in Y ; ::_thesis: verum
end;
hence  z in L \& O2 by A5, SETFAM_1:def_1; ::_thesis: verum
end;

theorem :: MMLQUERY:27
for X being set
for L being List of X
for O1, O2 being Operation of X holds L \& (O1 AND O2) = (L \& O1) AND (L \& O2)
proof
let X be set ; ::_thesis: for L being List of X
for O1, O2 being Operation of X holds L \& (O1 AND O2) = (L \& O1) AND (L \& O2)
let L be List of X; ::_thesis: for O1, O2 being Operation of X holds L \& (O1 AND O2) = (L \& O1) AND (L \& O2)
let O1, O2 be Operation of X; ::_thesis: L \& (O1 AND O2) = (L \& O1) AND (L \& O2)
 ( L \& (O1 AND O2) c= L \& O1 & L \& (O1 AND O2) c= L \& O2 ) by XBOOLE_1:17, Th81;
hence  L \& (O1 AND O2) c= (L \& O1) AND (L \& O2) by XBOOLE_1:19; :: according to XBOOLE_0:def_10 ::_thesis: (L \& O1) AND (L \& O2) c= L \& (O1 AND O2)
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in (L \& O1) AND (L \& O2) or z in L \& (O1 AND O2) )
assume  z in (L \& O1) AND (L \& O2) ; ::_thesis: z in L \& (O1 AND O2)
then A5: ( z in L \& O1 & z in L \& O2 ) by XBOOLE_0:def_4;
now__::_thesis:_(__{__(x_._(O1_AND_O2))_where_x_is_Element_of_X_:_x_in_L__}__<>_{}_&_(_for_Y_being_set_st_Y_in__{__(x_._(O1_AND_O2))_where_x_is_Element_of_X_:_x_in_L__}__holds_
z_in_Y_)_)
set O = O1 AND O2;
set c = the Element of L;
  {  (x . O1) where x is Element of X : x in L  }  <> {} by A5, SETFAM_1:def_1;
then consider c being set  such that
A1: c in  {  (x . O1) where x is Element of X : x in L  }  by XBOOLE_0:def_1;
consider a being Element of X such that
A2: ( c = a . O1 & a in L ) by A1;
 a . (O1 AND O2) in  {  (x . (O1 AND O2)) where x is Element of X : x in L  }  by A2;
hence   {  (x . (O1 AND O2)) where x is Element of X : x in L  }  <> {} ; ::_thesis: for Y being set st Y in  {  (x . (O1 AND O2)) where x is Element of X : x in L  }  holds
z in Y
let Y be set ; ::_thesis: ( Y in  {  (x . (O1 AND O2)) where x is Element of X : x in L  }  implies z in Y )
assume  Y in  {  (x . (O1 AND O2)) where x is Element of X : x in L  }  ; ::_thesis: z in Y
then consider x being Element of X such that
A3: ( Y = x . (O1 AND O2) & x in L ) ;
A4: Y = (x . O1) AND (x . O2) by A3, RELSET_2:11;
 x . O1 in  {  (y . O1) where y is Element of X : y in L  }  by A3;
then A6: z in x . O1 by A5, SETFAM_1:def_1;
 x . O2 in  {  (y . O2) where y is Element of X : y in L  }  by A3;
then  z in x . O2 by A5, SETFAM_1:def_1;
hence  z in Y by A4, A6, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  z in L \& (O1 AND O2) by SETFAM_1:def_1; ::_thesis: verum
end;

theorem :: MMLQUERY:28
for X being set
for L1, L2 being List of X
for O being Operation of X st L1 <> {} & L1 c= L2 holds
L2 \& O c= L1 \& O
proof
let X be set ; ::_thesis: for L1, L2 being List of X
for O being Operation of X st L1 <> {} & L1 c= L2 holds
L2 \& O c= L1 \& O
let L1, L2 be List of X; ::_thesis: for O being Operation of X st L1 <> {} & L1 c= L2 holds
L2 \& O c= L1 \& O
let O be Operation of X; ::_thesis: ( L1 <> {} & L1 c= L2 implies L2 \& O c= L1 \& O )
assume Z0: L1 <> {} ; ::_thesis: ( not L1 c= L2 or L2 \& O c= L1 \& O )
assume Z1: L1 c= L2 ; ::_thesis: L2 \& O c= L1 \& O
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L2 \& O or z in L1 \& O )
assume A0: z in L2 \& O ; ::_thesis: z in L1 \& O
now__::_thesis:_(__{__(x_._O)_where_x_is_Element_of_X_:_x_in_L1__}__<>_{}_&_(_for_Y_being_set_st_Y_in__{__(x_._O)_where_x_is_Element_of_X_:_x_in_L1__}__holds_
z_in_Y_)_)
set c = the Element of L1;
 the Element of L1 in L1 by Z0;
then reconsider c = the Element of L1 as Element of X ;
 c . O in  {  (x . O) where x is Element of X : x in L1  }  by Z0;
hence   {  (x . O) where x is Element of X : x in L1  }  <> {} ; ::_thesis: for Y being set st Y in  {  (x . O) where x is Element of X : x in L1  }  holds
z in Y
let Y be set ; ::_thesis: ( Y in  {  (x . O) where x is Element of X : x in L1  }  implies z in Y )
assume  Y in  {  (x . O) where x is Element of X : x in L1  }  ; ::_thesis: z in Y
then consider x being Element of X such that
A3: ( Y = x . O & x in L1 ) ;
 Y in  {  (a . O) where a is Element of X : a in L2  }  by A3, Z1;
hence  z in Y by A0, SETFAM_1:def_1; ::_thesis: verum
end;
hence  z in L1 \& O by SETFAM_1:def_1; ::_thesis: verum
end;

begin

theorem Th3a: :: MMLQUERY:29
for X being set
for O1, O2 being Operation of X st ( for x being Element of X holds x . O1 = x . O2 ) holds
O1 = O2
proof
let X be set ; ::_thesis: for O1, O2 being Operation of X st ( for x being Element of X holds x . O1 = x . O2 ) holds
O1 = O2
let O1, O2 be Operation of X; ::_thesis: ( ( for x being Element of X holds x . O1 = x . O2 ) implies O1 = O2 )
assume Z0: for x being Element of X holds x . O1 = x . O2 ; ::_thesis: O1 = O2
let a, b be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [a,b] in O1 or [a,b] in O2 ) & ( not [a,b] in O2 or [a,b] in O1 ) )
thus  ( [a,b] in O1 implies [a,b] in O2 ) ::_thesis: ( not [a,b] in O2 or [a,b] in O1 )
proof
assume A1: [a,b] in O1 ; ::_thesis: [a,b] in O2
reconsider a = a, b = b as Element of X by A1, ZFMISC_1:87;
 b in a . O1 by A1, RELAT_1:169;
then  b in a . O2 by Z0;
hence  [a,b] in O2 by RELAT_1:169; ::_thesis: verum
end;
assume A1: [a,b] in O2 ; ::_thesis: [a,b] in O1
then A2: ( a in X & b in X ) by ZFMISC_1:87;
reconsider a = a, b = b as Element of X by A1, ZFMISC_1:87;
reconsider L = {a} as Subset of X by A2, ZFMISC_1:31;
 b in a . O2 by A1, RELAT_1:169;
then  b in a . O1 by Z0;
hence  [a,b] in O1 by RELAT_1:169; ::_thesis: verum
end;

theorem Th3: :: MMLQUERY:30
for X being set
for O1, O2 being Operation of X st ( for L being List of X holds L | O1 = L | O2 ) holds
O1 = O2
proof
let X be set ; ::_thesis: for O1, O2 being Operation of X st ( for L being List of X holds L | O1 = L | O2 ) holds
O1 = O2
let O1, O2 be Operation of X; ::_thesis: ( ( for L being List of X holds L | O1 = L | O2 ) implies O1 = O2 )
assume Z0: for L being List of X holds L | O1 = L | O2 ; ::_thesis: O1 = O2
now__::_thesis:_for_x_being_Element_of_X_holds_x_._O1_=_x_._O2
let x be Element of X; ::_thesis: b1 . O1 = b1 . O2
percases ( X <> {} or X = {} ) ;
suppose X <> {} ; ::_thesis: b1 . O1 = b1 . O2
then reconsider L = {x} as Subset of X by ZFMISC_1:31;
thus x . O1 = L | O1
.= x . O2 by Z0 ; ::_thesis: verum
end;
suppose X = {} ; ::_thesis: b1 . O1 = b1 . O2
hence  x . O1 = x . O2 ; ::_thesis: verum
end;
end;
end;
hence  O1 = O2 by Th3a; ::_thesis: verum
end;

definition
let X be set ;
let O be Operation of X;
func NOT O ->  Operation of X means :DEFNOT: :: MMLQUERY:def 15
 for L being List of X holds L | it = union  {  (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L  }  ;
existence
 ex b1 being Operation of X st
for L being List of X holds L | b1 = union  {  (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L  }
proof
defpred S1[ set , set ] means ( Im (O,$1) = {} & $2 = $1 );
consider O1 being Relation such that
A1: for a, b being set holds
( [a,b] in O1 iff ( a in X & b in X & S1[a,b] ) ) from RELAT_1:sch_1();
 O1 c= [:X,X:]
proof
let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in O1 or [x,y] in [:X,X:] )
assume  [x,y] in O1 ; ::_thesis: [x,y] in [:X,X:]
then  ( x in X & y in X ) by A1;
hence  [x,y] in [:X,X:] by ZFMISC_1:87; ::_thesis: verum
end;
then reconsider O1 = O1 as Operation of X ;
take  O1 ; ::_thesis: for L being List of X holds L | O1 = union  {  (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L  }
let L be List of X; ::_thesis: L | O1 = union  {  (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L  }
thus  L | O1 c= union  {  (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L  }  :: according to XBOOLE_0:def_10 ::_thesis: union  {  (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L  }  c= L | O1
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in L | O1 or a in union  {  (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L  }  )
assume  a in L | O1 ; ::_thesis: a in union  {  (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L  }
then consider b being Element of X such that
A2: ( a in b . O1 & b in L ) by Th1;
 [b,a] in O1 by A2, RELAT_1:169;
then A3: ( a = b & b . O = {} ) by A1;
then  a in {b} by TARSKI:def_1;
then A4: a in IFEQ ((b . O),{},{b},{}) by A3, FUNCOP_1:def_8;
 IFEQ ((b . O),{},{b},{}) in  {  (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L  }  by A2;
hence  a in union  {  (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L  }  by A4, TARSKI:def_4; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in union  {  (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L  }  or a in L | O1 )
assume  a in union  {  (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L  }  ; ::_thesis: a in L | O1
then consider A being set  such that
A5: ( a in A & A in  {  (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L  }  ) by TARSKI:def_4;
consider x being Element of X such that
A6: ( A = IFEQ ((x . O),{},{x},{}) & x in L ) by A5;
A7: x . O = {} by A5, A6, FUNCOP_1:def_8;
then  A = {x} by A6, FUNCOP_1:def_8;
then  a = x by A5, TARSKI:def_1;
then  [x,a] in O1 by A1, A6, A7;
hence  a in L | O1 by A6, RELAT_1:def_13; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Operation of X st ( for L being List of X holds L | b1 = union  {  (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L  }  ) & ( for L being List of X holds L | b2 = union  {  (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L  }  ) holds
b1 = b2
proof
let O1, O2 be Operation of X; ::_thesis: ( ( for L being List of X holds L | O1 = union  {  (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L  }  ) & ( for L being List of X holds L | O2 = union  {  (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L  }  ) implies O1 = O2 )
assume that
A1: for L being List of X holds L | O1 = union  {  (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L  }  and
A2: for L being List of X holds L | O2 = union  {  (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L  }  ; ::_thesis: O1 = O2
now__::_thesis:_for_L_being_List_of_X_holds_L_|_O1_=_L_|_O2
let L be List of X; ::_thesis: L | O1 = L | O2
thus L | O1 = union  {  (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L  }  by A1
.= L | O2 by A2 ; ::_thesis: verum
end;
hence  O1 = O2 by Th3; ::_thesis: verum
end;
end;

:: deftheorem DEFNOT defines NOT MMLQUERY:def_15_:_
 for X being set
for O, b3 being Operation of X holds
( b3 = NOT O iff for L being List of X holds L | b3 = union  {  (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L  }  );

notation
let X be set ;
let O1, O2 be Operation of X;
synonym O1 AND O2 for X /\ O1;
synonym O1 OR O2 for X \/ O1;
synonym O1 BUTNOT O2 for X \ O1;
synonym O1 | O2 for X * O1;
end;

definition
let X be set ;
let O1, O2 be Operation of X;
:: original: AND
redefine funcO1 AND O2 ->  Operation of X means :: MMLQUERY:def 16
 for L being List of X holds L | it = union  {  ((x . O1) AND (x . O2)) where x is Element of X : x in L  }  ;
coherence
 O2 AND is Operation of X
proof
thus  O1 /\ O2 is Subset of [:X,X:] ; ::_thesis: verum
end;
compatibility
 for b1 being Operation of X holds
( b1 = O2 AND iff for L being List of X holds L | b1 = union  {  ((x . O1) AND (x . O2)) where x is Element of X : x in L  }  )
proof
AA: for O being Operation of X st O = O2 AND holds
for L being List of X holds L | O = union  {  ((x . O1) AND (x . O2)) where x is Element of X : x in L  }
proof
let O be Operation of X; ::_thesis: ( O = O2 AND implies for L being List of X holds L | O = union  {  ((x . O1) AND (x . O2)) where x is Element of X : x in L  }  )
assume A0: O = O1 /\ O2 ; ::_thesis: for L being List of X holds L | O = union  {  ((x . O1) AND (x . O2)) where x is Element of X : x in L  }
defpred S1[ set , set ] means ( [$1,$2] in O1 & [$1,$2] in O2 );
let L be List of X; ::_thesis: L | O = union  {  ((x . O1) AND (x . O2)) where x is Element of X : x in L  }
thus  L | O c= union  {  ((x . O1) AND (x . O2)) where x is Element of X : x in L  }  :: according to XBOOLE_0:def_10 ::_thesis: union  {  ((x . O1) AND (x . O2)) where x is Element of X : x in L  }  c= L | O
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L | O or z in union  {  ((x . O1) AND (x . O2)) where x is Element of X : x in L  }  )
assume  z in L | O ; ::_thesis: z in union  {  ((x . O1) AND (x . O2)) where x is Element of X : x in L  }
then consider y being set  such that
A2: ( [y,z] in O & y in L ) by RELAT_1:def_13;
reconsider y = y, z = z as Element of X by A2, ZFMISC_1:87;
 ( [y,z] in O1 & [y,z] in O2 ) by A0, A2, XBOOLE_0:def_4;
then  ( z in y . O1 & z in y . O2 ) by RELAT_1:169;
then  ( z in (y . O1) AND (y . O2) & (y . O1) AND (y . O2) in  {  ((x . O1) AND (x . O2)) where x is Element of X : x in L  }  ) by A2, XBOOLE_0:def_4;
hence  z in union  {  ((x . O1) AND (x . O2)) where x is Element of X : x in L  }  by TARSKI:def_4; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union  {  ((x . O1) AND (x . O2)) where x is Element of X : x in L  }  or z in L | O )
assume  z in union  {  ((x . O1) AND (x . O2)) where x is Element of X : x in L  }  ; ::_thesis: z in L | O
then consider Y being set  such that
A3: ( z in Y & Y in  {  ((x . O1) AND (x . O2)) where x is Element of X : x in L  }  ) by TARSKI:def_4;
consider x being Element of X such that
A4: ( Y = (x . O1) AND (x . O2) & x in L ) by A3;
A5: ( z in x . O1 & z in x . O2 ) by A3, A4, XBOOLE_0:def_4;
reconsider z = z as Element of X by A3, A4;
 ( [x,z] in O1 & [x,z] in O2 ) by A5, RELAT_1:169;
then  [x,z] in O by A0, XBOOLE_0:def_4;
hence  z in L | O by A4, RELAT_1:def_13; ::_thesis: verum
end;
let O be Operation of X; ::_thesis: ( O = O2 AND iff for L being List of X holds L | O = union  {  ((x . O1) AND (x . O2)) where x is Element of X : x in L  }  )
thus  ( O = O2 AND implies for L being List of X holds L | O = union  {  ((x . O1) AND (x . O2)) where x is Element of X : x in L  }  ) by AA; ::_thesis: ( ( for L being List of X holds L | O = union  {  ((x . O1) AND (x . O2)) where x is Element of X : x in L  }  ) implies O = O2 AND )
assume A6: for L being List of X holds L | O = union  {  ((x . O1) AND (x . O2)) where x is Element of X : x in L  }  ; ::_thesis: O = O2 AND
now__::_thesis:_for_L_being_List_of_X_holds_L_|_O_=_L_|_(O1_/\_O2)
let L be List of X; ::_thesis: L | O = L | (O1 /\ O2)
thus L | O = union  {  ((x . O1) AND (x . O2)) where x is Element of X : x in L  }  by A6
.= L | (O1 /\ O2) by AA ; ::_thesis: verum
end;
hence  O = O2 AND by Th3; ::_thesis: verum
end;
:: original: OR
redefine funcO1 OR O2 ->  Operation of X means :: MMLQUERY:def 17
 for L being List of X holds L | it = union  {  ((x . O1) OR (x . O2)) where x is Element of X : x in L  }  ;
coherence
 O2 OR is Operation of X
proof
thus  O1 \/ O2 is Subset of [:X,X:] ; ::_thesis: verum
end;
compatibility
 for b1 being Operation of X holds
( b1 = O2 OR iff for L being List of X holds L | b1 = union  {  ((x . O1) OR (x . O2)) where x is Element of X : x in L  }  )
proof
AA: for O being Operation of X st O = O2 OR holds
for L being List of X holds L | O = union  {  ((x . O1) OR (x . O2)) where x is Element of X : x in L  }
proof
let O be Operation of X; ::_thesis: ( O = O2 OR implies for L being List of X holds L | O = union  {  ((x . O1) OR (x . O2)) where x is Element of X : x in L  }  )
assume A0: O = O1 \/ O2 ; ::_thesis: for L being List of X holds L | O = union  {  ((x . O1) OR (x . O2)) where x is Element of X : x in L  }
defpred S1[ set , set ] means ( [$1,$2] in O1 or [$1,$2] in O2 );
let L be List of X; ::_thesis: L | O = union  {  ((x . O1) OR (x . O2)) where x is Element of X : x in L  }
thus  L | O c= union  {  ((x . O1) OR (x . O2)) where x is Element of X : x in L  }  :: according to XBOOLE_0:def_10 ::_thesis: union  {  ((x . O1) OR (x . O2)) where x is Element of X : x in L  }  c= L | O
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L | O or z in union  {  ((x . O1) OR (x . O2)) where x is Element of X : x in L  }  )
assume  z in L | O ; ::_thesis: z in union  {  ((x . O1) OR (x . O2)) where x is Element of X : x in L  }
then consider y being set  such that
A2: ( [y,z] in O & y in L ) by RELAT_1:def_13;
reconsider y = y, z = z as Element of X by A2, ZFMISC_1:87;
 ( [y,z] in O1 or [y,z] in O2 ) by A0, A2, XBOOLE_0:def_3;
then  ( z in y . O1 or z in y . O2 ) by RELAT_1:169;
then  ( z in (y . O1) OR (y . O2) & (y . O1) OR (y . O2) in  {  ((x . O1) OR (x . O2)) where x is Element of X : x in L  }  ) by A2, XBOOLE_0:def_3;
hence  z in union  {  ((x . O1) OR (x . O2)) where x is Element of X : x in L  }  by TARSKI:def_4; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union  {  ((x . O1) OR (x . O2)) where x is Element of X : x in L  }  or z in L | O )
assume  z in union  {  ((x . O1) OR (x . O2)) where x is Element of X : x in L  }  ; ::_thesis: z in L | O
then consider Y being set  such that
A3: ( z in Y & Y in  {  ((x . O1) OR (x . O2)) where x is Element of X : x in L  }  ) by TARSKI:def_4;
consider x being Element of X such that
A4: ( Y = (x . O1) OR (x . O2) & x in L ) by A3;
A5: ( z in x . O1 or z in x . O2 ) by A3, A4, XBOOLE_0:def_3;
reconsider z = z as Element of X by A3, A4;
 ( [x,z] in O1 or [x,z] in O2 ) by A5, RELAT_1:169;
then  [x,z] in O by A0, XBOOLE_0:def_3;
hence  z in L | O by A4, RELAT_1:def_13; ::_thesis: verum
end;
let O be Operation of X; ::_thesis: ( O = O2 OR iff for L being List of X holds L | O = union  {  ((x . O1) OR (x . O2)) where x is Element of X : x in L  }  )
thus  ( O = O2 OR implies for L being List of X holds L | O = union  {  ((x . O1) OR (x . O2)) where x is Element of X : x in L  }  ) by AA; ::_thesis: ( ( for L being List of X holds L | O = union  {  ((x . O1) OR (x . O2)) where x is Element of X : x in L  }  ) implies O = O2 OR )
assume A6: for L being List of X holds L | O = union  {  ((x . O1) OR (x . O2)) where x is Element of X : x in L  }  ; ::_thesis: O = O2 OR
now__::_thesis:_for_L_being_List_of_X_holds_L_|_O_=_L_|_(O1_\/_O2)
let L be List of X; ::_thesis: L | O = L | (O1 \/ O2)
thus L | O = union  {  ((x . O1) OR (x . O2)) where x is Element of X : x in L  }  by A6
.= L | (O1 \/ O2) by AA ; ::_thesis: verum
end;
hence  O = O2 OR by Th3; ::_thesis: verum
end;
:: original: BUTNOT
redefine funcO1 BUTNOT O2 ->  Operation of X means :: MMLQUERY:def 18
 for L being List of X holds L | it = union  {  ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L  }  ;
coherence
 O2 BUTNOT is Operation of X
proof
thus  O1 \ O2 is Subset of [:X,X:] ; ::_thesis: verum
end;
compatibility
 for b1 being Operation of X holds
( b1 = O2 BUTNOT iff for L being List of X holds L | b1 = union  {  ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L  }  )
proof
AA: for O being Operation of X st O = O2 BUTNOT holds
for L being List of X holds L | O = union  {  ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L  }
proof
let O be Operation of X; ::_thesis: ( O = O2 BUTNOT implies for L being List of X holds L | O = union  {  ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L  }  )
assume A0: O = O1 \ O2 ; ::_thesis: for L being List of X holds L | O = union  {  ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L  }
defpred S1[ set , set ] means ( [$1,$2] in O1 & not [$1,$2] in O2 );
let L be List of X; ::_thesis: L | O = union  {  ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L  }
thus  L | O c= union  {  ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L  }  :: according to XBOOLE_0:def_10 ::_thesis: union  {  ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L  }  c= L | O
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L | O or z in union  {  ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L  }  )
assume  z in L | O ; ::_thesis: z in union  {  ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L  }
then consider y being set  such that
A2: ( [y,z] in O & y in L ) by RELAT_1:def_13;
reconsider y = y, z = z as Element of X by A2, ZFMISC_1:87;
 ( [y,z] in O1 & [y,z] nin O2 ) by A0, A2, XBOOLE_0:def_5;
then  ( z in y . O1 & z nin y . O2 ) by RELAT_1:169;
then  ( z in (y . O1) BUTNOT (y . O2) & (y . O1) BUTNOT (y . O2) in  {  ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L  }  ) by A2, XBOOLE_0:def_5;
hence  z in union  {  ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L  }  by TARSKI:def_4; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union  {  ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L  }  or z in L | O )
assume  z in union  {  ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L  }  ; ::_thesis: z in L | O
then consider Y being set  such that
A3: ( z in Y & Y in  {  ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L  }  ) by TARSKI:def_4;
consider x being Element of X such that
A4: ( Y = (x . O1) BUTNOT (x . O2) & x in L ) by A3;
A5: ( z in x . O1 & z nin x . O2 ) by A3, A4, XBOOLE_0:def_5;
reconsider z = z as Element of X by A3, A4;
 ( [x,z] in O1 & [x,z] nin O2 ) by A5, RELAT_1:169;
then  [x,z] in O by A0, XBOOLE_0:def_5;
hence  z in L | O by A4, RELAT_1:def_13; ::_thesis: verum
end;
let O be Operation of X; ::_thesis: ( O = O2 BUTNOT iff for L being List of X holds L | O = union  {  ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L  }  )
thus  ( O = O2 BUTNOT implies for L being List of X holds L | O = union  {  ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L  }  ) by AA; ::_thesis: ( ( for L being List of X holds L | O = union  {  ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L  }  ) implies O = O2 BUTNOT )
assume A6: for L being List of X holds L | O = union  {  ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L  }  ; ::_thesis: O = O2 BUTNOT
now__::_thesis:_for_L_being_List_of_X_holds_L_|_O_=_L_|_(O1_\_O2)
let L be List of X; ::_thesis: L | O = L | (O1 \ O2)
thus L | O = union  {  ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L  }  by A6
.= L | (O1 \ O2) by AA ; ::_thesis: verum
end;
hence  O = O2 BUTNOT by Th3; ::_thesis: verum
end;
:: original: |
redefine funcO1 | O2 ->  Operation of X means :: MMLQUERY:def 19
 for L being List of X holds L | it = (L | O1) | O2;
coherence
 O2 | is Operation of X
proof
thus  O1 * O2 is Relation of X ; ::_thesis: verum
end;
compatibility
 for b1 being Operation of X holds
( b1 = O2 | iff for L being List of X holds L | b1 = (L | O1) | O2 )
proof
let O be Operation of X; ::_thesis: ( O = O2 | iff for L being List of X holds L | O = (L | O1) | O2 )
thus  ( O = O2 | implies for L being List of X holds L | O = (L | O1) | O2 ) by RELAT_1:126; ::_thesis: ( ( for L being List of X holds L | O = (L | O1) | O2 ) implies O = O2 | )
assume A1: for L being List of X holds L | O = (L | O1) | O2 ; ::_thesis: O = O2 |
now__::_thesis:_for_L_being_List_of_X_holds_L_|_O_=_L_|_(O1_*_O2)
let L be List of X; ::_thesis: L | O = L | (O1 * O2)
thus L | O = (L | O1) | O2 by A1
.= L | (O1 * O2) by RELAT_1:126 ; ::_thesis: verum
end;
hence  O = O2 | by Th3; ::_thesis: verum
end;
funcO1 \& O2 ->  Operation of X means :DefAmp: :: MMLQUERY:def 20
 for L being List of X holds L | it = union  {  ((x . O1) \& O2) where x is Element of X : x in L  }  ;
existence
 ex b1 being Operation of X st
for L being List of X holds L | b1 = union  {  ((x . O1) \& O2) where x is Element of X : x in L  }
proof
defpred S1[ set , set ] means  ex x being Element of X st
( $1 = x & $2 in (x . O1) \& O2 );
consider O being Relation such that
A1: for z, s being set holds
( [z,s] in O iff ( z in X & s in X & S1[z,s] ) ) from RELAT_1:sch_1();
 O c= [:X,X:]
proof
let z be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [z,b1] in O or [z,b1] in [:X,X:] )
let s be set ; ::_thesis: ( not [z,s] in O or [z,s] in [:X,X:] )
assume  [z,s] in O ; ::_thesis: [z,s] in [:X,X:]
then  ( z in X & s in X ) by A1;
hence  [z,s] in [:X,X:] by ZFMISC_1:87; ::_thesis: verum
end;
then reconsider O = O as Operation of X ;
take  O ; ::_thesis: for L being List of X holds L | O = union  {  ((x . O1) \& O2) where x is Element of X : x in L  }
let L be List of X; ::_thesis: L | O = union  {  ((x . O1) \& O2) where x is Element of X : x in L  }
thus  L | O c= union  {  ((x . O1) \& O2) where x is Element of X : x in L  }  :: according to XBOOLE_0:def_10 ::_thesis: union  {  ((x . O1) \& O2) where x is Element of X : x in L  }  c= L | O
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L | O or z in union  {  ((x . O1) \& O2) where x is Element of X : x in L  }  )
assume  z in L | O ; ::_thesis: z in union  {  ((x . O1) \& O2) where x is Element of X : x in L  }
then consider y being Element of X such that
A2: ( z in y . O & y in L ) by Th1;
 [y,z] in O by A2, RELAT_1:169;
then  ex x being Element of X st
( y = x & z in (x . O1) \& O2 ) by A1;
then  ( z in (y . O1) \& O2 & (y . O1) \& O2 in  {  ((x . O1) \& O2) where x is Element of X : x in L  }  ) by A2;
hence  z in union  {  ((x . O1) \& O2) where x is Element of X : x in L  }  by TARSKI:def_4; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union  {  ((x . O1) \& O2) where x is Element of X : x in L  }  or z in L | O )
assume  z in union  {  ((x . O1) \& O2) where x is Element of X : x in L  }  ; ::_thesis: z in L | O
then consider Y being set  such that
A3: ( z in Y & Y in  {  ((x . O1) \& O2) where x is Element of X : x in L  }  ) by TARSKI:def_4;
consider x being Element of X such that
A4: ( Y = (x . O1) \& O2 & x in L ) by A3;
 [x,z] in O by A1, A3, A4;
hence  z in L | O by A4, RELAT_1:def_13; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Operation of X st ( for L being List of X holds L | b1 = union  {  ((x . O1) \& O2) where x is Element of X : x in L  }  ) & ( for L being List of X holds L | b2 = union  {  ((x . O1) \& O2) where x is Element of X : x in L  }  ) holds
b1 = b2
proof
let R1, R2 be Operation of X; ::_thesis: ( ( for L being List of X holds L | R1 = union  {  ((x . O1) \& O2) where x is Element of X : x in L  }  ) & ( for L being List of X holds L | R2 = union  {  ((x . O1) \& O2) where x is Element of X : x in L  }  ) implies R1 = R2 )
assume that
A1: for L being List of X holds L | R1 = union  {  ((x . O1) \& O2) where x is Element of X : x in L  }  and
A2: for L being List of X holds L | R2 = union  {  ((x . O1) \& O2) where x is Element of X : x in L  }  ; ::_thesis: R1 = R2
now__::_thesis:_for_L_being_List_of_X_holds_L_|_R1_=_L_|_R2
let L be List of X; ::_thesis: L | R1 = L | R2
thus L | R1 = union  {  ((x . O1) \& O2) where x is Element of X : x in L  }  by A1
.= L | R2 by A2 ; ::_thesis: verum
end;
hence  R1 = R2 by Th3; ::_thesis: verum
end;
end;

:: deftheorem  defines AND MMLQUERY:def_16_:_
 for X being set
for O1, O2, b4 being Operation of X holds
( b4 = O1 AND O2 iff for L being List of X holds L | b4 = union  {  ((x . O1) AND (x . O2)) where x is Element of X : x in L  }  );

:: deftheorem  defines OR MMLQUERY:def_17_:_
 for X being set
for O1, O2, b4 being Operation of X holds
( b4 = O1 OR O2 iff for L being List of X holds L | b4 = union  {  ((x . O1) OR (x . O2)) where x is Element of X : x in L  }  );

:: deftheorem  defines BUTNOT MMLQUERY:def_18_:_
 for X being set
for O1, O2, b4 being Operation of X holds
( b4 = O1 BUTNOT O2 iff for L being List of X holds L | b4 = union  {  ((x . O1) BUTNOT (x . O2)) where x is Element of X : x in L  }  );

:: deftheorem  defines | MMLQUERY:def_19_:_
 for X being set
for O1, O2, b4 being Operation of X holds
( b4 = O1 | O2 iff for L being List of X holds L | b4 = (L | O1) | O2 );

:: deftheorem DefAmp defines \& MMLQUERY:def_20_:_
 for X being set
for O1, O2, b4 being Operation of X holds
( b4 = O1 \& O2 iff for L being List of X holds L | b4 = union  {  ((x . O1) \& O2) where x is Element of X : x in L  }  );

theorem :: MMLQUERY:31
for X being set
for x being Element of X
for O1, O2 being Operation of X holds x . (O1 AND O2) = (x . O1) AND (x . O2) by RELSET_2:11;

theorem :: MMLQUERY:32
for X being set
for x being Element of X
for O1, O2 being Operation of X holds x . (O1 OR O2) = (x . O1) OR (x . O2) by RELSET_2:10;

theorem :: MMLQUERY:33
for X being set
for x being Element of X
for O1, O2 being Operation of X holds x . (O1 BUTNOT O2) = (x . O1) BUTNOT (x . O2) by RELSET_2:12;

theorem :: MMLQUERY:34
for X being set
for x being Element of X
for O1, O2 being Operation of X holds x . (O1 | O2) = (x . O1) | O2 by RELAT_1:126;

theorem Th25: :: MMLQUERY:35
for X being set
for x being Element of X
for O1, O2 being Operation of X holds x . (O1 \& O2) = (x . O1) \& O2
proof
let X be set ; ::_thesis: for x being Element of X
for O1, O2 being Operation of X holds x . (O1 \& O2) = (x . O1) \& O2
let x be Element of X; ::_thesis: for O1, O2 being Operation of X holds x . (O1 \& O2) = (x . O1) \& O2
let O1, O2 be Operation of X; ::_thesis: x . (O1 \& O2) = (x . O1) \& O2
percases ( X = {} or X <> {} ) ;
suppose X = {} ; ::_thesis: x . (O1 \& O2) = (x . O1) \& O2
then  ( x . (O1 \& O2) = {} & (x . O1) \& O2 = {} ) ;
hence  x . (O1 \& O2) = (x . O1) \& O2 ; ::_thesis: verum
end;
suppose X <> {} ; ::_thesis: x . (O1 \& O2) = (x . O1) \& O2
then reconsider L = {x} as List of X by ZFMISC_1:31;
A1:  {  ((a . O1) \& O2) where a is Element of X : a in L  }  = {((x . O1) \& O2)}
proof
thus   {  ((a . O1) \& O2) where a is Element of X : a in L  }  c= {((x . O1) \& O2)} :: according to XBOOLE_0:def_10 ::_thesis: {((x . O1) \& O2)} c=  {  ((a . O1) \& O2) where a is Element of X : a in L  }
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  ((a . O1) \& O2) where a is Element of X : a in L  }  or z in {((x . O1) \& O2)} )
assume  z in  {  ((a . O1) \& O2) where a is Element of X : a in L  }  ; ::_thesis: z in {((x . O1) \& O2)}
then consider a being Element of X such that
A2: ( z = (a . O1) \& O2 & a in L ) ;
 a = x by A2, TARSKI:def_1;
hence  z in {((x . O1) \& O2)} by A2, TARSKI:def_1; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in {((x . O1) \& O2)} or z in  {  ((a . O1) \& O2) where a is Element of X : a in L  }  )
assume  z in {((x . O1) \& O2)} ; ::_thesis: z in  {  ((a . O1) \& O2) where a is Element of X : a in L  }
then  ( z = (x . O1) \& O2 & x in L ) by TARSKI:def_1;
hence  z in  {  ((a . O1) \& O2) where a is Element of X : a in L  }  ; ::_thesis: verum
end;
thus x . (O1 \& O2) = union  {  ((a . O1) \& O2) where a is Element of X : a in L  }  by DefAmp
.= (x . O1) \& O2 by A1, ZFMISC_1:25 ; ::_thesis: verum
end;
end;
end;

theorem Th4: :: MMLQUERY:36
for z, s, X being set
for O being Operation of X holds
( [z,s] in NOT O iff ( z = s & z in X & z nin dom O ) )
proof
let z, s, X be set ; ::_thesis: for O being Operation of X holds
( [z,s] in NOT O iff ( z = s & z in X & z nin dom O ) )
let O be Operation of X; ::_thesis: ( [z,s] in NOT O iff ( z = s & z in X & z nin dom O ) )
thus  ( [z,s] in NOT O implies ( z = s & z in X & z nin dom O ) ) ::_thesis: ( z = s & z in X & z nin dom O implies [z,s] in NOT O )
proof
assume A7: [z,s] in NOT O ; ::_thesis: ( z = s & z in X & z nin dom O )
then  ( s in Im ((NOT O),z) & z in X ) by RELAT_1:169, ZFMISC_1:87;
then  ( s in (NOT O) .: {z} & {z} c= X ) by ZFMISC_1:31;
then  s in union  {  (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in {z}  }  by DEFNOT;
then consider Y being set  such that
A1: ( s in Y & Y in  {  (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in {z}  }  ) by TARSKI:def_4;
consider x being Element of X such that
A2: ( Y = IFEQ ((x . O),{},{x},{}) & x in {z} ) by A1;
A3: x = z by A2, TARSKI:def_1;
A5: x . O = {} by A1, A2, FUNCOP_1:def_8;
then  s in {x} by A1, A2, FUNCOP_1:def_8;
then  ( s = x & ( for s being set holds [x,s] nin O ) ) by A5, RELAT_1:169, TARSKI:def_1;
hence  ( z = s & z in X & z nin dom O ) by A3, A7, XTUPLE_0:def_12, ZFMISC_1:87; ::_thesis: verum
end;
assume A6: ( z = s & z in X & z nin dom O ) ; ::_thesis: [z,s] in NOT O
then reconsider z = z as Element of X ;
 z . O c= {}
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in z . O or y in {} )
assume  y in z . O ; ::_thesis: y in {}
then  [z,y] in O by RELAT_1:169;
hence  y in {} by A6, XTUPLE_0:def_12; ::_thesis: verum
end;
then  z . O = {} ;
then A7: IFEQ ((z . O),{},{z},{}) = {z} by FUNCOP_1:def_8;
A8: z in {z} by TARSKI:def_1;
reconsider L = {z} as Subset of X by A6, ZFMISC_1:31;
 {z} in  {  (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in {z}  }  by A7, A8;
then  z in union  {  (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in {z}  }  by A8, TARSKI:def_4;
then  z in L | (NOT O) by DEFNOT;
then  z in z . (NOT O) ;
hence  [z,s] in NOT O by A6, RELAT_1:169; ::_thesis: verum
end;

theorem Th5: :: MMLQUERY:37
for X being set
for O being Operation of X holds NOT O = id (X \ (dom O))
proof
let X be set ; ::_thesis: for O being Operation of X holds NOT O = id (X \ (dom O))
let O be Operation of X; ::_thesis: NOT O = id (X \ (dom O))
let z be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds
( ( not [z,b1] in NOT O or [z,b1] in id (X \ (dom O)) ) & ( not [z,b1] in id (X \ (dom O)) or [z,b1] in NOT O ) )
let s be set ; ::_thesis: ( ( not [z,s] in NOT O or [z,s] in id (X \ (dom O)) ) & ( not [z,s] in id (X \ (dom O)) or [z,s] in NOT O ) )
thus  ( [z,s] in NOT O implies [z,s] in id (X \ (dom O)) ) ::_thesis: ( not [z,s] in id (X \ (dom O)) or [z,s] in NOT O )
proof
assume  [z,s] in NOT O ; ::_thesis: [z,s] in id (X \ (dom O))
then A1: ( z = s & z in X & z nin dom O ) by Th4;
then  z in X \ (dom O) by XBOOLE_0:def_5;
hence  [z,s] in id (X \ (dom O)) by A1, RELAT_1:def_10; ::_thesis: verum
end;
assume  [z,s] in id (X \ (dom O)) ; ::_thesis: [z,s] in NOT O
then A2: ( z = s & z in X \ (dom O) ) by RELAT_1:def_10;
then  ( z in X & z nin dom O ) by XBOOLE_0:def_5;
hence  [z,s] in NOT O by A2, Th4; ::_thesis: verum
end;

theorem Th6: :: MMLQUERY:38
for X being set
for O being Operation of X holds dom (NOT (NOT O)) = dom O
proof
let X be set ; ::_thesis: for O being Operation of X holds dom (NOT (NOT O)) = dom O
let O be Operation of X; ::_thesis: dom (NOT (NOT O)) = dom O
thus  dom (NOT (NOT O)) = dom (id (X \ (dom (NOT O)))) by Th5
.= X \ (dom (NOT O)) by RELAT_1:45
.= X \ (dom (id (X \ (dom O)))) by Th5
.= X \ (X \ (dom O)) by RELAT_1:45
.= X /\ (dom O) by XBOOLE_1:48
.= dom O by XBOOLE_1:28 ; ::_thesis: verum
end;

theorem :: MMLQUERY:39
for X being set
for L being List of X
for O being Operation of X holds L WHERE (NOT (NOT O)) = L WHERE O
proof
let X be set ; ::_thesis: for L being List of X
for O being Operation of X holds L WHERE (NOT (NOT O)) = L WHERE O
let L be List of X; ::_thesis: for O being Operation of X holds L WHERE (NOT (NOT O)) = L WHERE O
let O be Operation of X; ::_thesis: L WHERE (NOT (NOT O)) = L WHERE O
thus  L WHERE (NOT (NOT O)) c= L WHERE O :: according to XBOOLE_0:def_10 ::_thesis: L WHERE O c= L WHERE (NOT (NOT O))
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L WHERE (NOT (NOT O)) or z in L WHERE O )
assume A0: z in L WHERE (NOT (NOT O)) ; ::_thesis: z in L WHERE O
then reconsider x = z as Element of X ;
A1: ( x in L & x . (NOT (NOT O)) <> {} ) by A0, ThW;
then  x in dom (NOT (NOT O)) by RELAT_1:170;
then  x in dom O by Th6;
then  x . O <> {} by RELAT_1:170;
hence  z in L WHERE O by A1, ThW; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L WHERE O or z in L WHERE (NOT (NOT O)) )
assume A2: z in L WHERE O ; ::_thesis: z in L WHERE (NOT (NOT O))
then reconsider x = z as Element of X ;
A3: ( z in L & x . O <> {} ) by A2, ThW;
then  x in dom O by RELAT_1:170;
then  x in dom (NOT (NOT O)) by Th6;
then  x . (NOT (NOT O)) <> {} by RELAT_1:170;
hence  z in L WHERE (NOT (NOT O)) by A3, ThW; ::_thesis: verum
end;

theorem :: MMLQUERY:40
for X being set
for L being List of X
for O being Operation of X holds L WHEREeq (O,0) = L WHERE (NOT O)
proof
let X be set ; ::_thesis: for L being List of X
for O being Operation of X holds L WHEREeq (O,0) = L WHERE (NOT O)
let L be List of X; ::_thesis: for O being Operation of X holds L WHEREeq (O,0) = L WHERE (NOT O)
let O be Operation of X; ::_thesis: L WHEREeq (O,0) = L WHERE (NOT O)
thus  L WHEREeq (O,0) c= L WHERE (NOT O) :: according to XBOOLE_0:def_10 ::_thesis: L WHERE (NOT O) c= L WHEREeq (O,0)
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L WHEREeq (O,0) or z in L WHERE (NOT O) )
assume  z in L WHEREeq (O,0) ; ::_thesis: z in L WHERE (NOT O)
then consider x being Element of X such that
A1: ( z = x & card (x . O) = 0 & x in L ) ;
 x . O = {} by A1;
then  x nin dom O by RELAT_1:170;
then  [x,x] in NOT O by A1, Th4;
then  x,x in NOT O by Def1;
hence  z in L WHERE (NOT O) by A1; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L WHERE (NOT O) or z in L WHEREeq (O,0) )
assume  z in L WHERE (NOT O) ; ::_thesis: z in L WHEREeq (O,0)
then consider x being Element of X such that
A2: ( z = x & ex y being Element of X st
( x,y in NOT O & x in L ) ) ;
consider y being Element of X such that
A3: ( x,y in NOT O & x in L ) by A2;
 [x,y] in NOT O by A3, Def1;
then  ( x = y & x in X & x nin dom O ) by Th4;
then  x . O = {} by RELAT_1:170;
then  card (x . O) = 0 ;
hence  z in L WHEREeq (O,0) by A2; ::_thesis: verum
end;

theorem :: MMLQUERY:41
for X being set
for O being Operation of X holds NOT (NOT (NOT O)) = NOT O
proof
let X be set ; ::_thesis: for O being Operation of X holds NOT (NOT (NOT O)) = NOT O
let O be Operation of X; ::_thesis: NOT (NOT (NOT O)) = NOT O
thus  NOT (NOT (NOT O)) = id (X \ (dom (NOT (NOT O)))) by Th5
.= id (X \ (dom O)) by Th6
.= NOT O by Th5 ; ::_thesis: verum
end;

theorem :: MMLQUERY:42
for X being set
for O1, O2 being Operation of X holds (NOT O1) OR (NOT O2) c= NOT (O1 AND O2)
proof
let X be set ; ::_thesis: for O1, O2 being Operation of X holds (NOT O1) OR (NOT O2) c= NOT (O1 AND O2)
let O1, O2 be Operation of X; ::_thesis: (NOT O1) OR (NOT O2) c= NOT (O1 AND O2)
let z be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [z,b1] in (NOT O1) OR (NOT O2) or [z,b1] in NOT (O1 AND O2) )
let s be set ; ::_thesis: ( not [z,s] in (NOT O1) OR (NOT O2) or [z,s] in NOT (O1 AND O2) )
assume  [z,s] in (NOT O1) OR (NOT O2) ; ::_thesis: [z,s] in NOT (O1 AND O2)
then  ( [z,s] in NOT O1 or [z,s] in NOT O2 ) by XBOOLE_0:def_3;
then A1: ( s = z & z in X & ( z nin dom O1 or z nin dom O2 ) ) by Th4;
then  ( z nin (dom O1) /\ (dom O2) & dom (O1 AND O2) c= (dom O1) /\ (dom O2) ) by RELAT_1:2, XBOOLE_0:def_4;
then  z nin dom (O1 AND O2) ;
hence  [z,s] in NOT (O1 AND O2) by A1, Th4; ::_thesis: verum
end;

theorem :: MMLQUERY:43
for X being set
for O1, O2 being Operation of X holds NOT (O1 OR O2) = (NOT O1) AND (NOT O2)
proof
let X be set ; ::_thesis: for O1, O2 being Operation of X holds NOT (O1 OR O2) = (NOT O1) AND (NOT O2)
let O1, O2 be Operation of X; ::_thesis: NOT (O1 OR O2) = (NOT O1) AND (NOT O2)
let z be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds
( ( not [z,b1] in NOT (O1 OR O2) or [z,b1] in (NOT O1) AND (NOT O2) ) & ( not [z,b1] in (NOT O1) AND (NOT O2) or [z,b1] in NOT (O1 OR O2) ) )
let s be set ; ::_thesis: ( ( not [z,s] in NOT (O1 OR O2) or [z,s] in (NOT O1) AND (NOT O2) ) & ( not [z,s] in (NOT O1) AND (NOT O2) or [z,s] in NOT (O1 OR O2) ) )
thus  ( [z,s] in NOT (O1 OR O2) implies [z,s] in (NOT O1) AND (NOT O2) ) ::_thesis: ( not [z,s] in (NOT O1) AND (NOT O2) or [z,s] in NOT (O1 OR O2) )
proof
assume  [z,s] in NOT (O1 OR O2) ; ::_thesis: [z,s] in (NOT O1) AND (NOT O2)
then A1: ( z = s & z in X & z nin dom (O1 OR O2) ) by Th4;
then  z nin (dom O1) \/ (dom O2) by RELAT_1:1;
then  ( z nin dom O1 & z nin dom O2 ) by XBOOLE_0:def_3;
then  ( [z,s] in NOT O1 & [z,s] in NOT O2 ) by A1, Th4;
hence  [z,s] in (NOT O1) AND (NOT O2) by XBOOLE_0:def_4; ::_thesis: verum
end;
assume  [z,s] in (NOT O1) AND (NOT O2) ; ::_thesis: [z,s] in NOT (O1 OR O2)
then  ( [z,s] in NOT O1 & [z,s] in NOT O2 ) by XBOOLE_0:def_4;
then A1: ( z = s & z in X & z nin dom O1 & z nin dom O2 ) by Th4;
then  z nin (dom O1) \/ (dom O2) by XBOOLE_0:def_3;
then  z nin dom (O1 OR O2) by RELAT_1:1;
hence  [z,s] in NOT (O1 OR O2) by A1, Th4; ::_thesis: verum
end;

theorem :: MMLQUERY:44
for X being set
for O1, O2, O being Operation of X st dom O1 = X & dom O2 = X holds
(O1 OR O2) \& O = (O1 \& O) AND (O2 \& O)
proof
let X be set ; ::_thesis: for O1, O2, O being Operation of X st dom O1 = X & dom O2 = X holds
(O1 OR O2) \& O = (O1 \& O) AND (O2 \& O)
let O1, O2, O be Operation of X; ::_thesis: ( dom O1 = X & dom O2 = X implies (O1 OR O2) \& O = (O1 \& O) AND (O2 \& O) )
assume A0: ( dom O1 = X & dom O2 = X ) ; ::_thesis: (O1 OR O2) \& O = (O1 \& O) AND (O2 \& O)
let z be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds
( ( not [z,b1] in (O1 OR O2) \& O or [z,b1] in (O1 \& O) AND (O2 \& O) ) & ( not [z,b1] in (O1 \& O) AND (O2 \& O) or [z,b1] in (O1 OR O2) \& O ) )
let s be set ; ::_thesis: ( ( not [z,s] in (O1 OR O2) \& O or [z,s] in (O1 \& O) AND (O2 \& O) ) & ( not [z,s] in (O1 \& O) AND (O2 \& O) or [z,s] in (O1 OR O2) \& O ) )
thus  ( [z,s] in (O1 OR O2) \& O implies [z,s] in (O1 \& O) AND (O2 \& O) ) ::_thesis: ( not [z,s] in (O1 \& O) AND (O2 \& O) or [z,s] in (O1 OR O2) \& O )
proof
assume Z0: [z,s] in (O1 OR O2) \& O ; ::_thesis: [z,s] in (O1 \& O) AND (O2 \& O)
then reconsider z = z, s = s as Element of X by ZFMISC_1:87;
 s in z . ((O1 OR O2) \& O) by Z0, RELAT_1:169;
then  s in (z . (O1 OR O2)) \& O by Th25;
then  ( s in ((z . O1) OR (z . O2)) \& O & z . O1 <> {} & z . O2 <> {} ) by A0, RELAT_1:170, RELSET_2:10;
then  s in ((z . O1) \& O) AND ((z . O2) \& O) by Th17;
then  s in (z . (O1 \& O)) AND ((z . O2) \& O) by Th25;
then  s in (z . (O1 \& O)) AND (z . (O2 \& O)) by Th25;
then  s in z . ((O1 \& O) AND (O2 \& O)) by RELSET_2:11;
hence  [z,s] in (O1 \& O) AND (O2 \& O) by RELAT_1:169; ::_thesis: verum
end;
assume Z1: [z,s] in (O1 \& O) AND (O2 \& O) ; ::_thesis: [z,s] in (O1 OR O2) \& O
then reconsider z = z, s = s as Element of X by ZFMISC_1:87;
 s in z . ((O1 \& O) AND (O2 \& O)) by Z1, RELAT_1:169;
then  s in (z . (O1 \& O)) AND (z . (O2 \& O)) by RELSET_2:11;
then  s in (z . (O1 \& O)) AND ((z . O2) \& O) by Th25;
then  ( s in ((z . O1) \& O) AND ((z . O2) \& O) & z . O1 <> {} & z . O2 <> {} ) by Th25, A0, RELAT_1:170;
then  s in ((z . O1) OR (z . O2)) \& O by Th17;
then  s in (z . (O1 OR O2)) \& O by RELSET_2:10;
then  s in z . ((O1 OR O2) \& O) by Th25;
hence  [z,s] in (O1 OR O2) \& O by RELAT_1:169; ::_thesis: verum
end;

definition
let X be set ;
let O be Operation of X;
attrO is filtering  means :DEFFILT: :: MMLQUERY:def 21
O c= id X;
end;

:: deftheorem DEFFILT defines filtering MMLQUERY:def_21_:_
 for X being set
for O being Operation of X holds
( O is filtering iff O c= id X );

theorem Th20: :: MMLQUERY:45
for X being set
for O being Operation of X holds
( O is filtering iff O = id (dom O) )
proof
let X be set ; ::_thesis: for O being Operation of X holds
( O is filtering iff O = id (dom O) )
let O be Operation of X; ::_thesis: ( O is filtering iff O = id (dom O) )
thus  ( O is filtering implies O = id (dom O) ) ::_thesis: ( O = id (dom O) implies O is filtering )
proof
assume A1: O c= id X ; :: according to MMLQUERY:def_21 ::_thesis: O = id (dom O)
let z be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds
( ( not [z,b1] in O or [z,b1] in id (dom O) ) & ( not [z,b1] in id (dom O) or [z,b1] in O ) )
let s be set ; ::_thesis: ( ( not [z,s] in O or [z,s] in id (dom O) ) & ( not [z,s] in id (dom O) or [z,s] in O ) )
thus  ( [z,s] in O implies [z,s] in id (dom O) ) ::_thesis: ( not [z,s] in id (dom O) or [z,s] in O )
proof
assume  [z,s] in O ; ::_thesis: [z,s] in id (dom O)
then  ( z in dom O & z = s ) by A1, RELAT_1:def_10, XTUPLE_0:def_12;
hence  [z,s] in id (dom O) by RELAT_1:def_10; ::_thesis: verum
end;
assume  [z,s] in id (dom O) ; ::_thesis: [z,s] in O
then A2: ( z in dom O & z = s ) by RELAT_1:def_10;
then consider y being set  such that
A3: [z,y] in O by XTUPLE_0:def_12;
thus  [z,s] in O by A1, A2, A3, RELAT_1:def_10; ::_thesis: verum
end;
assume  O = id (dom O) ; ::_thesis: O is filtering
hence  O c= id X by SYSREL:15; :: according to MMLQUERY:def_21 ::_thesis: verum
end;

registration
let X be set ;
let O be Operation of X;
cluster NOT O ->  filtering ;
coherence
 NOT O is filtering
proof
 NOT O = id (X \ (dom O)) by Th5;
hence  NOT O c= id X by SYSREL:15; :: according to MMLQUERY:def_21 ::_thesis: verum
end;
end;

registration
let X be set ;
cluster Relation-like X -defined X -valued filtering for Element of bool [:X,X:];
existence
 ex b1 being Operation of X st b1 is filtering
proof
set O = the Operation of X;
take  NOT the Operation of X ; ::_thesis: NOT the Operation of X is filtering
thus  NOT the Operation of X is filtering ; ::_thesis: verum
end;
end;


registration
let X be set ;
let F be filtering Operation of X;
let O be Operation of X;
clusterO AND  ->  filtering for Operation of X;
coherence
 for b1 being Operation of X st b1 = F AND O holds
b1 is filtering
proof
let O1 be Operation of X; ::_thesis: ( O1 = F AND O implies O1 is filtering )
assume  O1 = F AND O ; ::_thesis: O1 is filtering
then  ( O1 c= F & F c= id X ) by DEFFILT, XBOOLE_1:17;
hence  O1 c= id X by XBOOLE_1:1; :: according to MMLQUERY:def_21 ::_thesis: verum
end;
clusterF AND  ->  filtering for Operation of X;
coherence
 for b1 being Operation of X st b1 = O AND F holds
b1 is filtering ;
clusterO BUTNOT  ->  filtering for Operation of X;
coherence
 for b1 being Operation of X st b1 = F BUTNOT O holds
b1 is filtering
proof
let O1 be Operation of X; ::_thesis: ( O1 = F BUTNOT O implies O1 is filtering )
assume  O1 = F BUTNOT O ; ::_thesis: O1 is filtering
then  ( O1 c= F & F c= id X ) by DEFFILT, XBOOLE_1:36;
hence  O1 c= id X by XBOOLE_1:1; :: according to MMLQUERY:def_21 ::_thesis: verum
end;
end;

registration
let X be set ;
let F1, F2 be filtering Operation of X;
clusterF2 OR  ->  filtering for Operation of X;
coherence
 for b1 being Operation of X st b1 = F1 OR F2 holds
b1 is filtering
proof
let O1 be Operation of X; ::_thesis: ( O1 = F1 OR F2 implies O1 is filtering )
assume A1: O1 = F1 OR F2 ; ::_thesis: O1 is filtering
 ( F1 c= id X & F2 c= id X ) by DEFFILT;
hence  O1 c= id X by A1, XBOOLE_1:8; :: according to MMLQUERY:def_21 ::_thesis: verum
end;
end;

theorem Th11: :: MMLQUERY:46
for X, z being set
for x being Element of X
for F being filtering Operation of X st z in x . F holds
z = x
proof
let X, z be set ; ::_thesis: for x being Element of X
for F being filtering Operation of X st z in x . F holds
z = x
let x be Element of X; ::_thesis: for F being filtering Operation of X st z in x . F holds
z = x
let F be filtering Operation of X; ::_thesis: ( z in x . F implies z = x )
assume  z in x . F ; ::_thesis: z = x
then  ( [x,z] in F & F c= id X ) by DEFFILT, RELAT_1:169;
hence  z = x by RELAT_1:def_10; ::_thesis: verum
end;

theorem :: MMLQUERY:47
for X being set
for L being List of X
for F being filtering Operation of X holds L | F = L WHERE F
proof
let X be set ; ::_thesis: for L being List of X
for F being filtering Operation of X holds L | F = L WHERE F
let L be List of X; ::_thesis: for F being filtering Operation of X holds L | F = L WHERE F
let F be filtering Operation of X; ::_thesis: L | F = L WHERE F
thus  L | F c= L WHERE F :: according to XBOOLE_0:def_10 ::_thesis: L WHERE F c= L | F
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L | F or z in L WHERE F )
assume  z in L | F ; ::_thesis: z in L WHERE F
then consider y being Element of X such that
A1: ( z in y . F & y in L ) by Th1;
 z = y by A1, Th11;
hence  z in L WHERE F by A1, ThW; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in L WHERE F or z in L | F )
assume A2: z in L WHERE F ; ::_thesis: z in L | F
then reconsider x = z as Element of X ;
A3: ( x in L & x . F <> {} ) by A2, ThW;
set y = the Element of x . F;
A4: [x, the Element of x . F] in F by A3, RELAT_1:169;
 F c= id X by DEFFILT;
then  x = the Element of x . F by A4, RELAT_1:def_10;
hence  z in L | F by A3, Th1; ::_thesis: verum
end;

theorem :: MMLQUERY:48
for X being set
for F being filtering Operation of X holds NOT (NOT F) = F
proof
let X be set ; ::_thesis: for F being filtering Operation of X holds NOT (NOT F) = F
let F be filtering Operation of X; ::_thesis: NOT (NOT F) = F
thus  NOT (NOT F) = id (X \ (dom (NOT F))) by Th5
.= id (X \ (dom (id (X \ (dom F))))) by Th5
.= id (X \ (X \ (dom F))) by RELAT_1:45
.= id (X /\ (dom F)) by XBOOLE_1:48
.= id (dom F) by XBOOLE_1:28
.= F by Th20 ; ::_thesis: verum
end;

theorem :: MMLQUERY:49
for X being set
for F1, F2 being filtering Operation of X holds NOT (F1 AND F2) = (NOT F1) OR (NOT F2)
proof
let X be set ; ::_thesis: for F1, F2 being filtering Operation of X holds NOT (F1 AND F2) = (NOT F1) OR (NOT F2)
let F1, F2 be filtering Operation of X; ::_thesis: NOT (F1 AND F2) = (NOT F1) OR (NOT F2)
A1: ( F1 = id (dom F1) & F2 = id (dom F2) ) by Th20;
NOT (F1 AND F2) = id (X \ (dom (F1 AND F2))) by Th5
.= id (X \ (dom (id ((dom F1) AND (dom F2))))) by A1, SYSREL:14
.= id (X \ ((dom F1) AND (dom F2))) by RELAT_1:45
.= id ((X \ (dom F1)) \/ (X \ (dom F2))) by XBOOLE_1:54
.= (id (X \ (dom F1))) \/ (id (X \ (dom F2))) by SYSREL:14
.= (NOT F1) \/ (id (X \ (dom F2))) by Th5 ;
hence  NOT (F1 AND F2) = (NOT F1) OR (NOT F2) by Th5; ::_thesis: verum
end;

theorem Th71: :: MMLQUERY:50
for X being set
for O being Operation of X holds dom (O OR (NOT O)) = X
proof
let X be set ; ::_thesis: for O being Operation of X holds dom (O OR (NOT O)) = X
let O be Operation of X; ::_thesis: dom (O OR (NOT O)) = X
thus  dom (O OR (NOT O)) = (dom O) OR (dom (NOT O)) by RELAT_1:1
.= (dom O) \/ (dom (id (X \ (dom O)))) by Th5
.= (dom O) OR (X \ (dom O)) by RELAT_1:45
.= (dom O) \/ X by XBOOLE_1:39
.= X by XBOOLE_1:12 ; ::_thesis: verum
end;

theorem :: MMLQUERY:51
for X being set
for F being filtering Operation of X holds F OR (NOT F) = id X
proof
let X be set ; ::_thesis: for F being filtering Operation of X holds F OR (NOT F) = id X
let F be filtering Operation of X; ::_thesis: F OR (NOT F) = id X
 ( dom (F OR (NOT F)) = X & F OR (NOT F) c= id X ) by Th71, DEFFILT;
hence  F OR (NOT F) = id X by SYSREL:17; ::_thesis: verum
end;

theorem Th72: :: MMLQUERY:52
for X being set
for O being Operation of X holds O AND (NOT O) = {}
proof
let X be set ; ::_thesis: for O being Operation of X holds O AND (NOT O) = {}
let O be Operation of X; ::_thesis: O AND (NOT O) = {}
 dom (O AND (NOT O)) = dom (O /\ (id (X \ (dom O)))) by Th5;
then A1: dom (O AND (NOT O)) c= (dom O) /\ (dom (id (X \ (dom O)))) by RELAT_1:2;
(dom O) /\ (dom (id (X \ (dom O)))) = (dom O) /\ (X \ (dom O)) by RELAT_1:45
.= ((dom O) /\ X) \ (dom O) by XBOOLE_1:49
.= (dom O) \ (dom O) by XBOOLE_1:28
.= {} by XBOOLE_1:37 ;
hence  O AND (NOT O) = {} by A1, RELAT_1:41, XBOOLE_1:3; ::_thesis: verum
end;

theorem :: MMLQUERY:53
for X being set
for O1, O2 being Operation of X holds (O1 OR O2) AND (NOT O1) c= O2
proof
let X be set ; ::_thesis: for O1, O2 being Operation of X holds (O1 OR O2) AND (NOT O1) c= O2
let O1, O2 be Operation of X; ::_thesis: (O1 OR O2) AND (NOT O1) c= O2
(O1 OR O2) AND (NOT O1) = (O1 AND (NOT O1)) OR (O2 AND (NOT O1)) by XBOOLE_1:23
.= {} \/ (O2 AND (NOT O1)) by Th72
.= O2 AND (NOT O1) ;
hence  (O1 OR O2) AND (NOT O1) c= O2 by XBOOLE_1:17; ::_thesis: verum
end;

begin

definition
let A be FinSequence;
let a be set ;
func #occurrences (a,A) ->  Nat equals :: MMLQUERY:def 22
 card  {  i where i is Element of NAT : ( i in dom A & a in A . i )  }  ;
coherence
 card  {  i where i is Element of NAT : ( i in dom A & a in A . i )  }  is Nat
proof
  {  i where i is Element of NAT : ( i in dom A & a in A . i )  }  c= dom A
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  i where i is Element of NAT : ( i in dom A & a in A . i )  }  or z in dom A )
assume  z in  {  i where i is Element of NAT : ( i in dom A & a in A . i )  }  ; ::_thesis: z in dom A
then  ex i being Element of NAT st
( z = i & i in dom A & a in A . i ) ;
hence  z in dom A ; ::_thesis: verum
end;
hence  card  {  i where i is Element of NAT : ( i in dom A & a in A . i )  }  is Nat ; ::_thesis: verum
end;
end;

:: deftheorem  defines #occurrences MMLQUERY:def_22_:_
 for A being FinSequence
for a being set holds #occurrences (a,A) = card  {  i where i is Element of NAT : ( i in dom A & a in A . i )  }  ;

theorem Th21: :: MMLQUERY:54
for A being FinSequence
for a being set holds #occurrences (a,A) <= len A
proof
let A be FinSequence; ::_thesis: for a being set holds #occurrences (a,A) <= len A
let a be set ; ::_thesis: #occurrences (a,A) <= len A
  {  i where i is Element of NAT : ( i in dom A & a in A . i )  }  c= dom A
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  i where i is Element of NAT : ( i in dom A & a in A . i )  }  or z in dom A )
assume  z in  {  i where i is Element of NAT : ( i in dom A & a in A . i )  }  ; ::_thesis: z in dom A
then  ex i being Element of NAT st
( z = i & i in dom A & a in A . i ) ;
hence  z in dom A ; ::_thesis: verum
end;
then  ( #occurrences (a,A) c= card (dom A) & dom A = Seg (len A) & card (Seg (len A)) = len A ) by CARD_1:11, FINSEQ_1:57, FINSEQ_1:def_3;
hence  #occurrences (a,A) <= len A by NAT_1:39; ::_thesis: verum
end;

theorem Th22: :: MMLQUERY:55
for A being FinSequence
for a being set holds
( ( A <> {} & #occurrences (a,A) = len A ) iff a in meet (rng A) )
proof
let A be FinSequence; ::_thesis: for a being set holds
( ( A <> {} & #occurrences (a,A) = len A ) iff a in meet (rng A) )
let a be set ; ::_thesis: ( ( A <> {} & #occurrences (a,A) = len A ) iff a in meet (rng A) )
A2:  {  i where i is Element of NAT : ( i in dom A & a in A . i )  }  c= dom A
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  i where i is Element of NAT : ( i in dom A & a in A . i )  }  or z in dom A )
assume  z in  {  i where i is Element of NAT : ( i in dom A & a in A . i )  }  ; ::_thesis: z in dom A
then  ex i being Element of NAT st
( z = i & i in dom A & a in A . i ) ;
hence  z in dom A ; ::_thesis: verum
end;
A6: ( dom A = Seg (len A) & card (Seg (len A)) = len A ) by FINSEQ_1:57, FINSEQ_1:def_3;
hereby  ::_thesis: ( a in meet (rng A) implies ( A <> {} & #occurrences (a,A) = len A ) )
assume  A <> {} ; ::_thesis: ( #occurrences (a,A) = len A implies a in meet (rng A) )
then A0: rng A <> {} by RELAT_1:41;
assume Z1: #occurrences (a,A) = len A ; ::_thesis: a in meet (rng A)
A1:  {  i where i is Element of NAT : ( i in dom A & a in A . i )  }  = dom A by Z1, A2, A6, CARD_FIN:1;
now__::_thesis:_for_z_being_set_st_z_in_rng_A_holds_
a_in_z
let z be set ; ::_thesis: ( z in rng A implies a in z )
assume  z in rng A ; ::_thesis: a in z
then consider s being set  such that
A3: ( s in dom A & z = A . s ) by FUNCT_1:def_3;
consider i being Element of NAT  such that
A4: ( s = i & i in dom A & a in A . i ) by A1, A3;
thus  a in z by A3, A4; ::_thesis: verum
end;
hence  a in meet (rng A) by A0, SETFAM_1:def_1; ::_thesis: verum
end;
assume Z2: a in meet (rng A) ; ::_thesis: ( A <> {} & #occurrences (a,A) = len A )
thus  A <> {} by Z2, RELAT_1:38, SETFAM_1:def_1; ::_thesis: #occurrences (a,A) = len A
 dom A c=  {  i where i is Element of NAT : ( i in dom A & a in A . i )  }
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in dom A or z in  {  i where i is Element of NAT : ( i in dom A & a in A . i )  }  )
assume A7: z in dom A ; ::_thesis: z in  {  i where i is Element of NAT : ( i in dom A & a in A . i )  }
then  A . z in rng A by FUNCT_1:def_3;
then  a in A . z by Z2, SETFAM_1:def_1;
hence  z in  {  i where i is Element of NAT : ( i in dom A & a in A . i )  }  by A7; ::_thesis: verum
end;
hence  #occurrences (a,A) = len A by A6, A2, XBOOLE_0:def_10; ::_thesis: verum
end;

definition
let A be FinSequence;
func max# A ->  Nat means :MAX: :: MMLQUERY:def 23
( ( for a being set holds #occurrences (a,A) <= it ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds
it <= n ) );
existence
 ex b1 being Nat st
( ( for a being set holds #occurrences (a,A) <= b1 ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds
b1 <= n ) )
proof
defpred S1[ Nat] means  for a being set holds #occurrences (a,A) <= $1;
 S1[ len A] by Th21;
then A1: ex n being Nat st S1[n] ;
consider n being Nat such that
A2: ( S1[n] & ( for m being Nat st S1[m] holds
n <= m ) ) from NAT_1:sch_5(A1);
take  n ; ::_thesis: ( ( for a being set holds #occurrences (a,A) <= n ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds
n <= n ) )
thus  ( ( for a being set holds #occurrences (a,A) <= n ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds
n <= n ) ) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Nat st ( for a being set holds #occurrences (a,A) <= b1 ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds
b1 <= n ) & ( for a being set holds #occurrences (a,A) <= b2 ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds
b2 <= n ) holds
b1 = b2
proof
let n1, n2 be Nat; ::_thesis: ( ( for a being set holds #occurrences (a,A) <= n1 ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds
n1 <= n ) & ( for a being set holds #occurrences (a,A) <= n2 ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds
n2 <= n ) implies n1 = n2 )
assume that
A1: ( ( for a being set holds #occurrences (a,A) <= n1 ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds
n1 <= n ) ) and
A2: ( ( for a being set holds #occurrences (a,A) <= n2 ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds
n2 <= n ) ) ; ::_thesis: n1 = n2
 ( n1 <= n2 & n2 <= n1 ) by A1, A2;
hence  n1 = n2 by XXREAL_0:1; ::_thesis: verum
end;
end;

:: deftheorem MAX defines max# MMLQUERY:def_23_:_
 for A being FinSequence
for b2 being Nat holds
( b2 = max# A iff ( ( for a being set holds #occurrences (a,A) <= b2 ) & ( for n being Nat st ( for a being set holds #occurrences (a,A) <= n ) holds
b2 <= n ) ) );

theorem Th23: :: MMLQUERY:56
for A being FinSequence holds max# A <= len A
proof
let A be FinSequence; ::_thesis: max# A <= len A
 for a being set holds #occurrences (a,A) <= len A by Th21;
hence  max# A <= len A by MAX; ::_thesis: verum
end;

theorem :: MMLQUERY:57
for A being FinSequence
for a being set st #occurrences (a,A) = len A holds
max# A = len A
proof
let A be FinSequence; ::_thesis: for a being set st #occurrences (a,A) = len A holds
max# A = len A
let a be set ; ::_thesis: ( #occurrences (a,A) = len A implies max# A = len A )
assume  #occurrences (a,A) = len A ; ::_thesis: max# A = len A
then  ( len A <= max# A & max# A <= len A ) by MAX, Th23;
hence  max# A = len A by XXREAL_0:1; ::_thesis: verum
end;

definition
let X be set ;
let A be FinSequence of bool X;
let n be Nat;
func ROUGH (A,n) ->  List of X equals :ROUGH1: :: MMLQUERY:def 24
 {  x where x is Element of X : n <= #occurrences (x,A)  }   if X <> {}
;
consistency
 for b1 being List of X holds verum ;
coherence
 ( X <> {} implies  {  x where x is Element of X : n <= #occurrences (x,A)  }  is List of X )
proof
assume A1: X <> {} ; ::_thesis:  {  x where x is Element of X : n <= #occurrences (x,A)  }  is List of X
  {  x where x is Element of X : n <= #occurrences (x,A)  }  c= X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  x where x is Element of X : n <= #occurrences (x,A)  }  or z in X )
assume  z in  {  x where x is Element of X : n <= #occurrences (x,A)  }  ; ::_thesis: z in X
then  ex x being Element of X st
( z = x & n <= #occurrences (x,A) ) ;
hence  z in X by A1; ::_thesis: verum
end;
hence   {  x where x is Element of X : n <= #occurrences (x,A)  }  is List of X ; ::_thesis: verum
end;
let m be Nat;
func ROUGH (A,n,m) ->  List of X equals :ROUGH2: :: MMLQUERY:def 25
 {  x where x is Element of X : ( n <= #occurrences (x,A) & #occurrences (x,A) <= m )  }   if X <> {}
;
consistency
 for b1 being List of X holds verum ;
coherence
 ( X <> {} implies  {  x where x is Element of X : ( n <= #occurrences (x,A) & #occurrences (x,A) <= m )  }  is List of X )
proof
assume A1: X <> {} ; ::_thesis:  {  x where x is Element of X : ( n <= #occurrences (x,A) & #occurrences (x,A) <= m )  }  is List of X
  {  x where x is Element of X : ( n <= #occurrences (x,A) & #occurrences (x,A) <= m )  }  c= X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  x where x is Element of X : ( n <= #occurrences (x,A) & #occurrences (x,A) <= m )  }  or z in X )
assume  z in  {  x where x is Element of X : ( n <= #occurrences (x,A) & #occurrences (x,A) <= m )  }  ; ::_thesis: z in X
then  ex x being Element of X st
( z = x & n <= #occurrences (x,A) & #occurrences (x,A) <= m ) ;
hence  z in X by A1; ::_thesis: verum
end;
hence   {  x where x is Element of X : ( n <= #occurrences (x,A) & #occurrences (x,A) <= m )  }  is List of X ; ::_thesis: verum
end;
end;

:: deftheorem ROUGH1 defines ROUGH MMLQUERY:def_24_:_
 for X being set
for A being FinSequence of bool X
for n being Nat st X <> {} holds
ROUGH (A,n) =  {  x where x is Element of X : n <= #occurrences (x,A)  }  ;

:: deftheorem ROUGH2 defines ROUGH MMLQUERY:def_25_:_
 for X being set
for A being FinSequence of bool X
for n, m being Nat st X <> {} holds
ROUGH (A,n,m) =  {  x where x is Element of X : ( n <= #occurrences (x,A) & #occurrences (x,A) <= m )  }  ;

definition
let X be set ;
let A be FinSequence of bool X;
func ROUGH A ->  List of X equals :: MMLQUERY:def 26
 ROUGH (A,(max# A));
coherence
 ROUGH (A,(max# A)) is List of X ;
end;

:: deftheorem  defines ROUGH MMLQUERY:def_26_:_
 for X being set
for A being FinSequence of bool X holds ROUGH A = ROUGH (A,(max# A));

theorem :: MMLQUERY:58
for X being set
for n being Nat
for A being FinSequence of bool X holds ROUGH (A,n,(len A)) = ROUGH (A,n)
proof
let X be set ; ::_thesis: for n being Nat
for A being FinSequence of bool X holds ROUGH (A,n,(len A)) = ROUGH (A,n)
let n be Nat; ::_thesis: for A being FinSequence of bool X holds ROUGH (A,n,(len A)) = ROUGH (A,n)
let A be FinSequence of bool X; ::_thesis: ROUGH (A,n,(len A)) = ROUGH (A,n)
thus  ROUGH (A,n,(len A)) c= ROUGH (A,n) :: according to XBOOLE_0:def_10 ::_thesis: ROUGH (A,n) c= ROUGH (A,n,(len A))
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in ROUGH (A,n,(len A)) or z in ROUGH (A,n) )
assume A1: z in ROUGH (A,n,(len A)) ; ::_thesis: z in ROUGH (A,n)
then  z in  {  x where x is Element of X : ( n <= #occurrences (x,A) & #occurrences (x,A) <= len A )  }  by ROUGH2;
then  ex x being Element of X st
( z = x & n <= #occurrences (x,A) & #occurrences (x,A) <= len A ) ;
then  z in  {  x where x is Element of X : n <= #occurrences (x,A)  }  ;
hence  z in ROUGH (A,n) by A1, ROUGH1; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in ROUGH (A,n) or z in ROUGH (A,n,(len A)) )
assume A2: z in ROUGH (A,n) ; ::_thesis: z in ROUGH (A,n,(len A))
then  z in  {  x where x is Element of X : n <= #occurrences (x,A)  }  by ROUGH1;
then consider x being Element of X such that
A3: ( z = x & n <= #occurrences (x,A) ) ;
 #occurrences (x,A) <= len A by Th21;
then  z in  {  x1 where x1 is Element of X : ( n <= #occurrences (x1,A) & #occurrences (x1,A) <= len A )  }  by A3;
hence  z in ROUGH (A,n,(len A)) by A2, ROUGH2; ::_thesis: verum
end;

theorem :: MMLQUERY:59
for X being set
for n, m being Nat
for A being FinSequence of bool X st n <= m holds
ROUGH (A,m) c= ROUGH (A,n)
proof
let X be set ; ::_thesis: for n, m being Nat
for A being FinSequence of bool X st n <= m holds
ROUGH (A,m) c= ROUGH (A,n)
let n, m be Nat; ::_thesis: for A being FinSequence of bool X st n <= m holds
ROUGH (A,m) c= ROUGH (A,n)
let A be FinSequence of bool X; ::_thesis: ( n <= m implies ROUGH (A,m) c= ROUGH (A,n) )
assume Z0: n <= m ; ::_thesis: ROUGH (A,m) c= ROUGH (A,n)
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in ROUGH (A,m) or z in ROUGH (A,n) )
assume A1: z in ROUGH (A,m) ; ::_thesis: z in ROUGH (A,n)
then  z in  {  x where x is Element of X : m <= #occurrences (x,A)  }  by ROUGH1;
then consider a being Element of X such that
A2: ( z = a & m <= #occurrences (a,A) ) ;
 n <= #occurrences (a,A) by Z0, A2, XXREAL_0:2;
then  z in  {  x where x is Element of X : n <= #occurrences (x,A)  }  by A2;
hence  z in ROUGH (A,n) by A1, ROUGH1; ::_thesis: verum
end;

theorem :: MMLQUERY:60
for X being set
for A being FinSequence of bool X
for n1, n2, m1, m2 being Nat st n1 <= m1 & n2 <= m2 holds
ROUGH (A,m1,n2) c= ROUGH (A,n1,m2)
proof
let X be set ; ::_thesis: for A being FinSequence of bool X
for n1, n2, m1, m2 being Nat st n1 <= m1 & n2 <= m2 holds
ROUGH (A,m1,n2) c= ROUGH (A,n1,m2)
let A be FinSequence of bool X; ::_thesis: for n1, n2, m1, m2 being Nat st n1 <= m1 & n2 <= m2 holds
ROUGH (A,m1,n2) c= ROUGH (A,n1,m2)
let n1, n2, m1, m2 be Nat; ::_thesis: ( n1 <= m1 & n2 <= m2 implies ROUGH (A,m1,n2) c= ROUGH (A,n1,m2) )
assume Z1: n1 <= m1 ; ::_thesis: ( not n2 <= m2 or ROUGH (A,m1,n2) c= ROUGH (A,n1,m2) )
assume Z2: n2 <= m2 ; ::_thesis: ROUGH (A,m1,n2) c= ROUGH (A,n1,m2)
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in ROUGH (A,m1,n2) or z in ROUGH (A,n1,m2) )
assume A1: z in ROUGH (A,m1,n2) ; ::_thesis: z in ROUGH (A,n1,m2)
then  z in  {  x where x is Element of X : ( m1 <= #occurrences (x,A) & #occurrences (x,A) <= n2 )  }  by ROUGH2;
then consider a being Element of X such that
A2: ( z = a & m1 <= #occurrences (a,A) & #occurrences (a,A) <= n2 ) ;
 ( n1 <= #occurrences (a,A) & #occurrences (a,A) <= m2 ) by Z1, Z2, A2, XXREAL_0:2;
then  z in  {  x where x is Element of X : ( n1 <= #occurrences (x,A) & #occurrences (x,A) <= m2 )  }  by A2;
hence  z in ROUGH (A,n1,m2) by A1, ROUGH2; ::_thesis: verum
end;

theorem :: MMLQUERY:61
for X being set
for n, m being Nat
for A being FinSequence of bool X holds ROUGH (A,n,m) c= ROUGH (A,n)
proof
let X be set ; ::_thesis: for n, m being Nat
for A being FinSequence of bool X holds ROUGH (A,n,m) c= ROUGH (A,n)
let n, m be Nat; ::_thesis: for A being FinSequence of bool X holds ROUGH (A,n,m) c= ROUGH (A,n)
let A be FinSequence of bool X; ::_thesis: ROUGH (A,n,m) c= ROUGH (A,n)
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in ROUGH (A,n,m) or z in ROUGH (A,n) )
assume A1: z in ROUGH (A,n,m) ; ::_thesis: z in ROUGH (A,n)
then  z in  {  x where x is Element of X : ( n <= #occurrences (x,A) & #occurrences (x,A) <= m )  }  by ROUGH2;
then  ex x being Element of X st
( z = x & n <= #occurrences (x,A) & #occurrences (x,A) <= m ) ;
then  z in  {  x where x is Element of X : n <= #occurrences (x,A)  }  ;
hence  z in ROUGH (A,n) by A1, ROUGH1; ::_thesis: verum
end;

theorem Th31: :: MMLQUERY:62
for X being set
for A being FinSequence of bool X st A <> {} holds
ROUGH (A,(len A)) = meet (rng A)
proof
let X be set ; ::_thesis: for A being FinSequence of bool X st A <> {} holds
ROUGH (A,(len A)) = meet (rng A)
let A be FinSequence of bool X; ::_thesis: ( A <> {} implies ROUGH (A,(len A)) = meet (rng A) )
assume A0: A <> {} ; ::_thesis: ROUGH (A,(len A)) = meet (rng A)
thus  ROUGH (A,(len A)) c= meet (rng A) :: according to XBOOLE_0:def_10 ::_thesis: meet (rng A) c= ROUGH (A,(len A))
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in ROUGH (A,(len A)) or z in meet (rng A) )
assume  z in ROUGH (A,(len A)) ; ::_thesis: z in meet (rng A)
then  z in  {  x where x is Element of X : len A <= #occurrences (x,A)  }  by ROUGH1;
then consider x being Element of X such that
A3: ( z = x & len A <= #occurrences (x,A) ) ;
 #occurrences (x,A) <= len A by Th21;
hence  z in meet (rng A) by A0, A3, Th22, XXREAL_0:1; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in meet (rng A) or z in ROUGH (A,(len A)) )
assume A2: z in meet (rng A) ; ::_thesis: z in ROUGH (A,(len A))
then  #occurrences (z,A) = len A by Th22;
then  z in  {  x where x is Element of X : len A <= #occurrences (x,A)  }  by A2;
hence  z in ROUGH (A,(len A)) by A2, ROUGH1; ::_thesis: verum
end;

theorem Th32: :: MMLQUERY:63
for X being set
for A being FinSequence of bool X holds ROUGH (A,1) = Union A
proof
let X be set ; ::_thesis: for A being FinSequence of bool X holds ROUGH (A,1) = Union A
let A be FinSequence of bool X; ::_thesis: ROUGH (A,1) = Union A
thus  ROUGH (A,1) c= Union A :: according to XBOOLE_0:def_10 ::_thesis: Union A c= ROUGH (A,1)
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in ROUGH (A,1) or z in Union A )
assume  z in ROUGH (A,1) ; ::_thesis: z in Union A
then  z in  {  x where x is Element of X : 1 <= #occurrences (x,A)  }  by ROUGH1;
then consider x being Element of X such that
A3: ( z = x & 1 <= #occurrences (x,A) ) ;
 1 = 0 + 1 ;
then  #occurrences (x,A) > 0 by A3, NAT_1:13;
then   {  i where i is Element of NAT : ( i in dom A & x in A . i )  }  <> {} ;
then consider s being set  such that
A2: s in  {  i where i is Element of NAT : ( i in dom A & x in A . i )  }  by XBOOLE_0:def_1;
consider i being Element of NAT  such that
A4: ( s = i & i in dom A & x in A . i ) by A2;
thus  z in Union A by A3, A4, CARD_5:2; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Union A or z in ROUGH (A,1) )
assume A6: z in Union A ; ::_thesis: z in ROUGH (A,1)
then consider s being set  such that
A5: ( s in dom A & z in A . s ) by CARD_5:2;
 s in  {  i where i is Element of NAT : ( i in dom A & z in A . i )  }  by A5;
then  card {s} c= #occurrences (z,A) by CARD_1:11, ZFMISC_1:31;
then  1 c= #occurrences (z,A) by CARD_1:30;
then  1 <= #occurrences (z,A) by NAT_1:39;
then  z in  {  x where x is Element of X : 1 <= #occurrences (x,A)  }  by A6;
hence  z in ROUGH (A,1) by A6, ROUGH1; ::_thesis: verum
end;

theorem :: MMLQUERY:64
for X being set
for L1, L2 being List of X holds ROUGH (<*L1,L2*>,2) = L1 AND L2
proof
let X be set ; ::_thesis: for L1, L2 being List of X holds ROUGH (<*L1,L2*>,2) = L1 AND L2
let L1, L2 be List of X; ::_thesis: ROUGH (<*L1,L2*>,2) = L1 AND L2
 ( len <*L1,L2*> = 2 & rng <*L1,L2*> = {L1,L2} & meet {L1,L2} = L1 AND L2 ) by FINSEQ_1:44, FINSEQ_2:127, SETFAM_1:11;
hence  ROUGH (<*L1,L2*>,2) = L1 AND L2 by Th31; ::_thesis: verum
end;

theorem :: MMLQUERY:65
for X being set
for L1, L2 being List of X holds ROUGH (<*L1,L2*>,1) = L1 OR L2
proof
let X be set ; ::_thesis: for L1, L2 being List of X holds ROUGH (<*L1,L2*>,1) = L1 OR L2
let L1, L2 be List of X; ::_thesis: ROUGH (<*L1,L2*>,1) = L1 OR L2
 ( len <*L1,L2*> = 2 & rng <*L1,L2*> = {L1,L2} & union {L1,L2} = L1 OR L2 & Union <*L1,L2*> = union (rng <*L1,L2*>) ) by CARD_3:def_4, FINSEQ_1:44, FINSEQ_2:127, ZFMISC_1:75;
hence  ROUGH (<*L1,L2*>,1) = L1 OR L2 by Th32; ::_thesis: verum
end;

begin

definition
attrc1 is strict ;
struct ConstructorDB  ->  1-sorted ;
aggrConstructorDB(# carrier, Constrs, ref-operation #) ->  ConstructorDB ;
sel Constrs c1 ->  List of the carrier of c1;
sel ref-operation c1 ->  Relation of the carrier of c1, the Constrs of c1;
end;

definition
let X be 1-sorted ;
mode List of X is List of the carrier of X;
mode Operation of X is Operation of the carrier of X;
end;

definition
let X be set ;
let S be Subset of X;
let R be Relation of X,S;
func @ R ->  Relation of X equals :: MMLQUERY:def 27
R;
coherence
 R is Relation of X
proof
 [:X,S:] c= [:X,X:] by ZFMISC_1:96;
hence  R is Relation of X by XBOOLE_1:1; ::_thesis: verum
end;
end;

:: deftheorem  defines @ MMLQUERY:def_27_:_
 for X being set
for S being Subset of X
for R being Relation of X,S holds @ R = R;

definition
let X be ConstructorDB ;
let a be Element of X;
funca ref  ->  List of X equals :: MMLQUERY:def 28
a . (@ the ref-operation of X);
coherence
 a . (@ the ref-operation of X) is List of X ;
funca occur  ->  List of X equals :: MMLQUERY:def 29
a . ((@ the ref-operation of X) ~);
coherence
 a . ((@ the ref-operation of X) ~) is List of X ;
end;

:: deftheorem  defines ref MMLQUERY:def_28_:_
 for X being ConstructorDB
for a being Element of X holds a ref = a . (@ the ref-operation of X);

:: deftheorem  defines occur MMLQUERY:def_29_:_
 for X being ConstructorDB
for a being Element of X holds a occur = a . ((@ the ref-operation of X) ~);

theorem Th10: :: MMLQUERY:66
for X being ConstructorDB
for x, y being Element of X holds
( x in y ref iff y in x occur )
proof
let X be ConstructorDB ; ::_thesis: for x, y being Element of X holds
( x in y ref iff y in x occur )
let x, y be Element of X; ::_thesis: ( x in y ref iff y in x occur )
hereby  ::_thesis: ( y in x occur implies x in y ref )
assume  x in y ref ; ::_thesis: y in x occur
then  [y,x] in @ the ref-operation of X by RELAT_1:169;
then  [x,y] in (@ the ref-operation of X) ~ by RELAT_1:def_7;
hence  y in x occur by RELAT_1:169; ::_thesis: verum
end;
assume  y in x occur ; ::_thesis: x in y ref
then  [x,y] in (@ the ref-operation of X) ~ by RELAT_1:169;
then  [y,x] in @ the ref-operation of X by RELAT_1:def_7;
hence  x in y ref by RELAT_1:169; ::_thesis: verum
end;

definition
let X be ConstructorDB ;
attrX is ref-finite  means :REFF: :: MMLQUERY:def 30
 for x being Element of X holds x ref is finite ;
end;

:: deftheorem REFF defines ref-finite MMLQUERY:def_30_:_
 for X being ConstructorDB holds
( X is ref-finite iff for x being Element of X holds x ref is finite );

registration
cluster finite  ->  ref-finite for ConstructorDB ;
coherence
 for b1 being ConstructorDB st b1 is finite holds
b1 is ref-finite
proof
let X be ConstructorDB ; ::_thesis: ( X is finite implies X is ref-finite )
assume A1: the carrier of X is finite ; :: according to STRUCT_0:def_11 ::_thesis: X is ref-finite
let x be Element of X; :: according to MMLQUERY:def_30 ::_thesis: x ref is finite
thus  x ref is finite by A1; ::_thesis: verum
end;
end;

registration
cluster non empty finite for ConstructorDB ;
existence
 ex b1 being ConstructorDB st
( b1 is finite & not b1 is empty )
proof
set X = the non empty finite set ;
set C = the Subset of the non empty finite set ;
set R = the Relation of the non empty finite set , the Subset of the non empty finite set ;
take D = ConstructorDB(# the non empty finite set , the Subset of the non empty finite set , the Relation of the non empty finite set , the Subset of the non empty finite set #); ::_thesis: ( D is finite & not D is empty )
thus  ( the carrier of D is finite & not the carrier of D is empty ) ; :: according to STRUCT_0:def_1,STRUCT_0:def_11 ::_thesis: verum
end;
end;

registration
let X be ref-finite ConstructorDB ;
let x be Element of X;
clusterx ref  ->  finite ;
coherence
 x ref is finite by REFF;
end;

definition
let X be ConstructorDB ;
let A be FinSequence of the Constrs of X;
func ATLEAST A ->  List of X equals :DefAtleast: :: MMLQUERY:def 31
 {  x where x is Element of X : rng A c= x ref  }   if  the carrier of X <> {}
;
consistency
 for b1 being List of X holds verum ;
coherence
 ( the carrier of X <> {} implies  {  x where x is Element of X : rng A c= x ref  }  is List of X )
proof
assume A1: the carrier of X <> {} ; ::_thesis:  {  x where x is Element of X : rng A c= x ref  }  is List of X
  {  x where x is Element of X : rng A c= x ref  }  c= the carrier of X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  x where x is Element of X : rng A c= x ref  }  or z in the carrier of X )
assume  z in  {  x where x is Element of X : rng A c= x ref  }  ; ::_thesis: z in the carrier of X
then  ex x being Element of X st
( z = x & rng A c= x ref ) ;
hence  z in the carrier of X by A1; ::_thesis: verum
end;
hence   {  x where x is Element of X : rng A c= x ref  }  is List of X ; ::_thesis: verum
end;
func ATMOST A ->  List of X equals :DefAtmost: :: MMLQUERY:def 32
 {  x where x is Element of X : x ref c= rng A  }   if  the carrier of X <> {}
;
consistency
 for b1 being List of X holds verum ;
coherence
 ( the carrier of X <> {} implies  {  x where x is Element of X : x ref c= rng A  }  is List of X )
proof
assume A1: the carrier of X <> {} ; ::_thesis:  {  x where x is Element of X : x ref c= rng A  }  is List of X
  {  x where x is Element of X : x ref c= rng A  }  c= the carrier of X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  x where x is Element of X : x ref c= rng A  }  or z in the carrier of X )
assume  z in  {  x where x is Element of X : x ref c= rng A  }  ; ::_thesis: z in the carrier of X
then  ex x being Element of X st
( z = x & x ref c= rng A ) ;
hence  z in the carrier of X by A1; ::_thesis: verum
end;
hence   {  x where x is Element of X : x ref c= rng A  }  is List of X ; ::_thesis: verum
end;
func EXACTLY A ->  List of X equals :DefExactly: :: MMLQUERY:def 33
 {  x where x is Element of X : x ref = rng A  }   if  the carrier of X <> {}
;
consistency
 for b1 being List of X holds verum ;
coherence
 ( the carrier of X <> {} implies  {  x where x is Element of X : x ref = rng A  }  is List of X )
proof
assume A1: the carrier of X <> {} ; ::_thesis:  {  x where x is Element of X : x ref = rng A  }  is List of X
  {  x where x is Element of X : x ref = rng A  }  c= the carrier of X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  x where x is Element of X : x ref = rng A  }  or z in the carrier of X )
assume  z in  {  x where x is Element of X : x ref = rng A  }  ; ::_thesis: z in the carrier of X
then  ex x being Element of X st
( z = x & x ref = rng A ) ;
hence  z in the carrier of X by A1; ::_thesis: verum
end;
hence   {  x where x is Element of X : x ref = rng A  }  is List of X ; ::_thesis: verum
end;
let n be Nat;
func ATLEAST- (A,n) ->  List of X equals :DefAtleastMinus: :: MMLQUERY:def 34
 {  x where x is Element of X : card ((rng A) \ (x ref)) <= n  }   if  the carrier of X <> {}
;
consistency
 for b1 being List of X holds verum ;
coherence
 ( the carrier of X <> {} implies  {  x where x is Element of X : card ((rng A) \ (x ref)) <= n  }  is List of X )
proof
assume A1: the carrier of X <> {} ; ::_thesis:  {  x where x is Element of X : card ((rng A) \ (x ref)) <= n  }  is List of X
  {  x where x is Element of X : card ((rng A) \ (x ref)) <= n  }  c= the carrier of X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  x where x is Element of X : card ((rng A) \ (x ref)) <= n  }  or z in the carrier of X )
assume  z in  {  x where x is Element of X : card ((rng A) \ (x ref)) <= n  }  ; ::_thesis: z in the carrier of X
then  ex x being Element of X st
( z = x & card ((rng A) \ (x ref)) <= n ) ;
hence  z in the carrier of X by A1; ::_thesis: verum
end;
hence   {  x where x is Element of X : card ((rng A) \ (x ref)) <= n  }  is List of X ; ::_thesis: verum
end;
end;

:: deftheorem DefAtleast defines ATLEAST MMLQUERY:def_31_:_
 for X being ConstructorDB
for A being FinSequence of the Constrs of X st the carrier of X <> {} holds
ATLEAST A =  {  x where x is Element of X : rng A c= x ref  }  ;

:: deftheorem DefAtmost defines ATMOST MMLQUERY:def_32_:_
 for X being ConstructorDB
for A being FinSequence of the Constrs of X st the carrier of X <> {} holds
ATMOST A =  {  x where x is Element of X : x ref c= rng A  }  ;

:: deftheorem DefExactly defines EXACTLY MMLQUERY:def_33_:_
 for X being ConstructorDB
for A being FinSequence of the Constrs of X st the carrier of X <> {} holds
EXACTLY A =  {  x where x is Element of X : x ref = rng A  }  ;

:: deftheorem DefAtleastMinus defines ATLEAST- MMLQUERY:def_34_:_
 for X being ConstructorDB
for A being FinSequence of the Constrs of X
for n being Nat st the carrier of X <> {} holds
ATLEAST- (A,n) =  {  x where x is Element of X : card ((rng A) \ (x ref)) <= n  }  ;

definition
let X be ref-finite ConstructorDB ;
let A be FinSequence of the Constrs of X;
let n be Nat;
func ATMOST+ (A,n) ->  List of X equals :DefAtmostPlus: :: MMLQUERY:def 35
 {  x where x is Element of X : card ((x ref) \ (rng A)) <= n  }   if  the carrier of X <> {}
;
consistency
 for b1 being List of X holds verum ;
coherence
 ( the carrier of X <> {} implies  {  x where x is Element of X : card ((x ref) \ (rng A)) <= n  }  is List of X )
proof
assume A1: the carrier of X <> {} ; ::_thesis:  {  x where x is Element of X : card ((x ref) \ (rng A)) <= n  }  is List of X
  {  x where x is Element of X : card ((x ref) \ (rng A)) <= n  }  c= the carrier of X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  x where x is Element of X : card ((x ref) \ (rng A)) <= n  }  or z in the carrier of X )
assume  z in  {  x where x is Element of X : card ((x ref) \ (rng A)) <= n  }  ; ::_thesis: z in the carrier of X
then  ex x being Element of X st
( z = x & card ((x ref) \ (rng A)) <= n ) ;
hence  z in the carrier of X by A1; ::_thesis: verum
end;
hence   {  x where x is Element of X : card ((x ref) \ (rng A)) <= n  }  is List of X ; ::_thesis: verum
end;
let m be Nat;
func EXACTLY+- (A,n,m) ->  List of X equals :DefExactlyPlusMinus: :: MMLQUERY:def 36
 {  x where x is Element of X : ( card ((x ref) \ (rng A)) <= n & card ((rng A) \ (x ref)) <= m )  }   if  the carrier of X <> {}
;
consistency
 for b1 being List of X holds verum ;
coherence
 ( the carrier of X <> {} implies  {  x where x is Element of X : ( card ((x ref) \ (rng A)) <= n & card ((rng A) \ (x ref)) <= m )  }  is List of X )
proof
assume A1: the carrier of X <> {} ; ::_thesis:  {  x where x is Element of X : ( card ((x ref) \ (rng A)) <= n & card ((rng A) \ (x ref)) <= m )  }  is List of X
  {  x where x is Element of X : ( card ((x ref) \ (rng A)) <= n & card ((rng A) \ (x ref)) <= m )  }  c= the carrier of X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  x where x is Element of X : ( card ((x ref) \ (rng A)) <= n & card ((rng A) \ (x ref)) <= m )  }  or z in the carrier of X )
assume  z in  {  x where x is Element of X : ( card ((x ref) \ (rng A)) <= n & card ((rng A) \ (x ref)) <= m )  }  ; ::_thesis: z in the carrier of X
then  ex x being Element of X st
( z = x & card ((x ref) \ (rng A)) <= n & card ((rng A) \ (x ref)) <= m ) ;
hence  z in the carrier of X by A1; ::_thesis: verum
end;
hence   {  x where x is Element of X : ( card ((x ref) \ (rng A)) <= n & card ((rng A) \ (x ref)) <= m )  }  is List of X ; ::_thesis: verum
end;
end;

:: deftheorem DefAtmostPlus defines ATMOST+ MMLQUERY:def_35_:_
 for X being ref-finite ConstructorDB
for A being FinSequence of the Constrs of X
for n being Nat st the carrier of X <> {} holds
ATMOST+ (A,n) =  {  x where x is Element of X : card ((x ref) \ (rng A)) <= n  }  ;

:: deftheorem DefExactlyPlusMinus defines EXACTLY+- MMLQUERY:def_36_:_
 for X being ref-finite ConstructorDB
for A being FinSequence of the Constrs of X
for n, m being Nat st the carrier of X <> {} holds
EXACTLY+- (A,n,m) =  {  x where x is Element of X : ( card ((x ref) \ (rng A)) <= n & card ((rng A) \ (x ref)) <= m )  }  ;


theorem Th41: :: MMLQUERY:67
for X being ConstructorDB
for A being FinSequence of the Constrs of X holds ATLEAST- (A,0) = ATLEAST A
proof
let X be ConstructorDB ; ::_thesis: for A being FinSequence of the Constrs of X holds ATLEAST- (A,0) = ATLEAST A
let A be FinSequence of the Constrs of X; ::_thesis: ATLEAST- (A,0) = ATLEAST A
percases ( the carrier of X = {} or the carrier of X <> {} ) ;
suppose the carrier of X = {} ; ::_thesis: ATLEAST- (A,0) = ATLEAST A
then  ( ATLEAST- (A,0) = {} & ATLEAST A = {} ) ;
hence  ATLEAST- (A,0) = ATLEAST A ; ::_thesis: verum
end;
supposeA0: the carrier of X <> {} ; ::_thesis: ATLEAST- (A,0) = ATLEAST A
then A1: ATLEAST- (A,0) =  {  x where x is Element of X : card ((rng A) \ (x ref)) <= 0  }  by DefAtleastMinus;
A2: ATLEAST A =  {  x where x is Element of X : rng A c= x ref  }  by A0, DefAtleast;
thus  ATLEAST- (A,0) c= ATLEAST A :: according to XBOOLE_0:def_10 ::_thesis: ATLEAST A c= ATLEAST- (A,0)
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in ATLEAST- (A,0) or z in ATLEAST A )
assume  z in ATLEAST- (A,0) ; ::_thesis: z in ATLEAST A
then consider x being Element of X such that
A3: ( z = x & card ((rng A) \ (x ref)) <= 0 ) by A1;
 (rng A) \ (x ref) = {} by A3, NAT_1:3;
then  rng A c= x ref by XBOOLE_1:37;
hence  z in ATLEAST A by A3, A2; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in ATLEAST A or z in ATLEAST- (A,0) )
assume  z in ATLEAST A ; ::_thesis: z in ATLEAST- (A,0)
then consider x being Element of X such that
A4: ( z = x & rng A c= x ref ) by A2;
 (rng A) \ (x ref) = {} by A4, XBOOLE_1:37;
then  card ((rng A) \ (x ref)) = 0 ;
hence  z in ATLEAST- (A,0) by A1, A4; ::_thesis: verum
end;
end;
end;

theorem Th42: :: MMLQUERY:68
for Y being ref-finite ConstructorDB
for B being FinSequence of the Constrs of Y holds ATMOST+ (B,0) = ATMOST B
proof
let Y be ref-finite ConstructorDB ; ::_thesis: for B being FinSequence of the Constrs of Y holds ATMOST+ (B,0) = ATMOST B
let B be FinSequence of the Constrs of Y; ::_thesis: ATMOST+ (B,0) = ATMOST B
percases ( the carrier of Y = {} or the carrier of Y <> {} ) ;
suppose the carrier of Y = {} ; ::_thesis: ATMOST+ (B,0) = ATMOST B
then  ( ATMOST+ (B,0) = {} & ATMOST B = {} ) ;
hence  ATMOST+ (B,0) = ATMOST B ; ::_thesis: verum
end;
supposeA0: the carrier of Y <> {} ; ::_thesis: ATMOST+ (B,0) = ATMOST B
then A1: ATMOST+ (B,0) =  {  y where y is Element of Y : card ((y ref) \ (rng B)) <= 0  }  by DefAtmostPlus;
A2: ATMOST B =  {  y where y is Element of Y : y ref c= rng B  }  by A0, DefAtmost;
thus  ATMOST+ (B,0) c= ATMOST B :: according to XBOOLE_0:def_10 ::_thesis: ATMOST B c= ATMOST+ (B,0)
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in ATMOST+ (B,0) or z in ATMOST B )
assume  z in ATMOST+ (B,0) ; ::_thesis: z in ATMOST B
then consider y being Element of Y such that
A3: ( z = y & card ((y ref) \ (rng B)) <= 0 ) by A1;
 (y ref) \ (rng B) = {} by A3, NAT_1:3;
then  y ref c= rng B by XBOOLE_1:37;
hence  z in ATMOST B by A3, A2; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in ATMOST B or z in ATMOST+ (B,0) )
assume  z in ATMOST B ; ::_thesis: z in ATMOST+ (B,0)
then consider y being Element of Y such that
A4: ( z = y & y ref c= rng B ) by A2;
 (y ref) \ (rng B) = {} by A4, XBOOLE_1:37;
then  card ((y ref) \ (rng B)) = 0 ;
hence  z in ATMOST+ (B,0) by A1, A4; ::_thesis: verum
end;
end;
end;

theorem Th43: :: MMLQUERY:69
for Y being ref-finite ConstructorDB
for B being FinSequence of the Constrs of Y holds EXACTLY+- (B,0,0) = EXACTLY B
proof
let Y be ref-finite ConstructorDB ; ::_thesis: for B being FinSequence of the Constrs of Y holds EXACTLY+- (B,0,0) = EXACTLY B
let B be FinSequence of the Constrs of Y; ::_thesis: EXACTLY+- (B,0,0) = EXACTLY B
percases ( the carrier of Y = {} or the carrier of Y <> {} ) ;
suppose the carrier of Y = {} ; ::_thesis: EXACTLY+- (B,0,0) = EXACTLY B
then  ( EXACTLY+- (B,0,0) = {} & EXACTLY B = {} ) ;
hence  EXACTLY+- (B,0,0) = EXACTLY B ; ::_thesis: verum
end;
supposeA0: the carrier of Y <> {} ; ::_thesis: EXACTLY+- (B,0,0) = EXACTLY B
then A1: EXACTLY+- (B,0,0) =  {  y where y is Element of Y : ( card ((y ref) \ (rng B)) <= 0 & card ((rng B) \ (y ref)) <= 0 )  }  by DefExactlyPlusMinus;
A2: EXACTLY B =  {  y where y is Element of Y : y ref = rng B  }  by A0, DefExactly;
thus  EXACTLY+- (B,0,0) c= EXACTLY B :: according to XBOOLE_0:def_10 ::_thesis: EXACTLY B c= EXACTLY+- (B,0,0)
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in EXACTLY+- (B,0,0) or z in EXACTLY B )
assume  z in EXACTLY+- (B,0,0) ; ::_thesis: z in EXACTLY B
then consider y being Element of Y such that
A3: ( z = y & card ((y ref) \ (rng B)) <= 0 & card ((rng B) \ (y ref)) <= 0 ) by A1;
 ( (y ref) \ (rng B) = {} & (rng B) \ (y ref) = {} ) by A3, NAT_1:3;
then  ( y ref c= rng B & rng B c= y ref ) by XBOOLE_1:37;
then  y ref = rng B by XBOOLE_0:def_10;
hence  z in EXACTLY B by A3, A2; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in EXACTLY B or z in EXACTLY+- (B,0,0) )
assume  z in EXACTLY B ; ::_thesis: z in EXACTLY+- (B,0,0)
then consider y being Element of Y such that
A4: ( z = y & y ref = rng B ) by A2;
 ( (y ref) \ (rng B) = {} & (rng B) \ (y ref) = {} ) by A4, XBOOLE_1:37;
then  ( card ((y ref) \ (rng B)) = 0 & card ((rng B) \ (y ref)) = 0 ) ;
hence  z in EXACTLY+- (B,0,0) by A1, A4; ::_thesis: verum
end;
end;
end;

theorem Th44: :: MMLQUERY:70
for n, m being Nat
for X being ConstructorDB
for A being FinSequence of the Constrs of X st n <= m holds
ATLEAST- (A,n) c= ATLEAST- (A,m)
proof
let n, m be Nat; ::_thesis: for X being ConstructorDB
for A being FinSequence of the Constrs of X st n <= m holds
ATLEAST- (A,n) c= ATLEAST- (A,m)
let X be ConstructorDB ; ::_thesis: for A being FinSequence of the Constrs of X st n <= m holds
ATLEAST- (A,n) c= ATLEAST- (A,m)
let A be FinSequence of the Constrs of X; ::_thesis: ( n <= m implies ATLEAST- (A,n) c= ATLEAST- (A,m) )
assume A1: n <= m ; ::_thesis: ATLEAST- (A,n) c= ATLEAST- (A,m)
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in ATLEAST- (A,n) or z in ATLEAST- (A,m) )
assume A2: z in ATLEAST- (A,n) ; ::_thesis: z in ATLEAST- (A,m)
then  z in  {  x where x is Element of X : card ((rng A) \ (x ref)) <= n  }  by DefAtleastMinus;
then consider x being Element of X such that
A3: ( z = x & card ((rng A) \ (x ref)) <= n ) ;
 card ((rng A) \ (x ref)) <= m by A1, A3, XXREAL_0:2;
then  x in  {  x1 where x1 is Element of X : card ((rng A) \ (x1 ref)) <= m  }  ;
hence  z in ATLEAST- (A,m) by A2, A3, DefAtleastMinus; ::_thesis: verum
end;

theorem Th45: :: MMLQUERY:71
for n, m being Nat
for Y being ref-finite ConstructorDB
for B being FinSequence of the Constrs of Y st n <= m holds
ATMOST+ (B,n) c= ATMOST+ (B,m)
proof
let n, m be Nat; ::_thesis: for Y being ref-finite ConstructorDB
for B being FinSequence of the Constrs of Y st n <= m holds
ATMOST+ (B,n) c= ATMOST+ (B,m)
let Y be ref-finite ConstructorDB ; ::_thesis: for B being FinSequence of the Constrs of Y st n <= m holds
ATMOST+ (B,n) c= ATMOST+ (B,m)
let B be FinSequence of the Constrs of Y; ::_thesis: ( n <= m implies ATMOST+ (B,n) c= ATMOST+ (B,m) )
assume A1: n <= m ; ::_thesis: ATMOST+ (B,n) c= ATMOST+ (B,m)
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in ATMOST+ (B,n) or z in ATMOST+ (B,m) )
assume A2: z in ATMOST+ (B,n) ; ::_thesis: z in ATMOST+ (B,m)
then  z in  {  y where y is Element of Y : card ((y ref) \ (rng B)) <= n  }  by DefAtmostPlus;
then consider y being Element of Y such that
A3: ( z = y & card ((y ref) \ (rng B)) <= n ) ;
 card ((y ref) \ (rng B)) <= m by A1, A3, XXREAL_0:2;
then  y in  {  x1 where x1 is Element of Y : card ((x1 ref) \ (rng B)) <= m  }  ;
hence  z in ATMOST+ (B,m) by A2, A3, DefAtmostPlus; ::_thesis: verum
end;

theorem Th46: :: MMLQUERY:72
for Y being ref-finite ConstructorDB
for B being FinSequence of the Constrs of Y
for n1, n2, m1, m2 being Nat st n1 <= m1 & n2 <= m2 holds
EXACTLY+- (B,n1,n2) c= EXACTLY+- (B,m1,m2)
proof
let Y be ref-finite ConstructorDB ; ::_thesis: for B being FinSequence of the Constrs of Y
for n1, n2, m1, m2 being Nat st n1 <= m1 & n2 <= m2 holds
EXACTLY+- (B,n1,n2) c= EXACTLY+- (B,m1,m2)
let B be FinSequence of the Constrs of Y; ::_thesis: for n1, n2, m1, m2 being Nat st n1 <= m1 & n2 <= m2 holds
EXACTLY+- (B,n1,n2) c= EXACTLY+- (B,m1,m2)
let n1, n2, m1, m2 be Nat; ::_thesis: ( n1 <= m1 & n2 <= m2 implies EXACTLY+- (B,n1,n2) c= EXACTLY+- (B,m1,m2) )
assume A1: ( n1 <= m1 & n2 <= m2 ) ; ::_thesis: EXACTLY+- (B,n1,n2) c= EXACTLY+- (B,m1,m2)
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in EXACTLY+- (B,n1,n2) or z in EXACTLY+- (B,m1,m2) )
assume A2: z in EXACTLY+- (B,n1,n2) ; ::_thesis: z in EXACTLY+- (B,m1,m2)
then  z in  {  y where y is Element of Y : ( card ((y ref) \ (rng B)) <= n1 & card ((rng B) \ (y ref)) <= n2 )  }  by DefExactlyPlusMinus;
then consider y being Element of Y such that
A3: ( z = y & card ((y ref) \ (rng B)) <= n1 & card ((rng B) \ (y ref)) <= n2 ) ;
 ( card ((y ref) \ (rng B)) <= m1 & card ((rng B) \ (y ref)) <= m2 ) by A1, A3, XXREAL_0:2;
then  y in  {  x1 where x1 is Element of Y : ( card ((x1 ref) \ (rng B)) <= m1 & card ((rng B) \ (x1 ref)) <= m2 )  }  ;
hence  z in EXACTLY+- (B,m1,m2) by A2, A3, DefExactlyPlusMinus; ::_thesis: verum
end;

theorem :: MMLQUERY:73
for n being Nat
for X being ConstructorDB
for A being FinSequence of the Constrs of X holds ATLEAST A c= ATLEAST- (A,n)
proof
let n be Nat; ::_thesis: for X being ConstructorDB
for A being FinSequence of the Constrs of X holds ATLEAST A c= ATLEAST- (A,n)
let X be ConstructorDB ; ::_thesis: for A being FinSequence of the Constrs of X holds ATLEAST A c= ATLEAST- (A,n)
let A be FinSequence of the Constrs of X; ::_thesis: ATLEAST A c= ATLEAST- (A,n)
 ( ATLEAST A = ATLEAST- (A,0) & 0 <= n ) by Th41, NAT_1:2;
hence  ATLEAST A c= ATLEAST- (A,n) by Th44; ::_thesis: verum
end;

theorem :: MMLQUERY:74
for n being Nat
for Y being ref-finite ConstructorDB
for B being FinSequence of the Constrs of Y holds ATMOST B c= ATMOST+ (B,n)
proof
let n be Nat; ::_thesis: for Y being ref-finite ConstructorDB
for B being FinSequence of the Constrs of Y holds ATMOST B c= ATMOST+ (B,n)
let Y be ref-finite ConstructorDB ; ::_thesis: for B being FinSequence of the Constrs of Y holds ATMOST B c= ATMOST+ (B,n)
let B be FinSequence of the Constrs of Y; ::_thesis: ATMOST B c= ATMOST+ (B,n)
 ( ATMOST B = ATMOST+ (B,0) & 0 <= n ) by Th42, NAT_1:2;
hence  ATMOST B c= ATMOST+ (B,n) by Th45; ::_thesis: verum
end;

theorem :: MMLQUERY:75
for n, m being Nat
for Y being ref-finite ConstructorDB
for B being FinSequence of the Constrs of Y holds EXACTLY B c= EXACTLY+- (B,n,m)
proof
let n, m be Nat; ::_thesis: for Y being ref-finite ConstructorDB
for B being FinSequence of the Constrs of Y holds EXACTLY B c= EXACTLY+- (B,n,m)
let Y be ref-finite ConstructorDB ; ::_thesis: for B being FinSequence of the Constrs of Y holds EXACTLY B c= EXACTLY+- (B,n,m)
let B be FinSequence of the Constrs of Y; ::_thesis: EXACTLY B c= EXACTLY+- (B,n,m)
 ( EXACTLY B = EXACTLY+- (B,0,0) & 0 <= n & 0 <= m ) by Th43, NAT_1:2;
hence  EXACTLY B c= EXACTLY+- (B,n,m) by Th46; ::_thesis: verum
end;

theorem :: MMLQUERY:76
for X being ConstructorDB
for A being FinSequence of the Constrs of X holds EXACTLY A = (ATLEAST A) AND (ATMOST A)
proof
let X be ConstructorDB ; ::_thesis: for A being FinSequence of the Constrs of X holds EXACTLY A = (ATLEAST A) AND (ATMOST A)
let A be FinSequence of the Constrs of X; ::_thesis: EXACTLY A = (ATLEAST A) AND (ATMOST A)
thus  EXACTLY A c= (ATLEAST A) AND (ATMOST A) :: according to XBOOLE_0:def_10 ::_thesis: (ATLEAST A) AND (ATMOST A) c= EXACTLY A
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in EXACTLY A or z in (ATLEAST A) AND (ATMOST A) )
assume A1: z in EXACTLY A ; ::_thesis: z in (ATLEAST A) AND (ATMOST A)
then  z in  {  x where x is Element of X : x ref = rng A  }  by DefExactly;
then consider x being Element of X such that
A2: ( z = x & x ref = rng A ) ;
 z in  {  y where y is Element of X : rng A c= y ref  }  by A2;
then A3: z in ATLEAST A by A1, DefAtleast;
 z in  {  y where y is Element of X : y ref c= rng A  }  by A2;
then  z in ATMOST A by A1, DefAtmost;
hence  z in (ATLEAST A) AND (ATMOST A) by A3, XBOOLE_0:def_4; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in (ATLEAST A) AND (ATMOST A) or z in EXACTLY A )
assume A6: z in (ATLEAST A) AND (ATMOST A) ; ::_thesis: z in EXACTLY A
then A4: ( z in ATLEAST A & z in ATMOST A ) by XBOOLE_0:def_4;
then  z in  {  y where y is Element of X : y ref c= rng A  }  by DefAtmost;
then consider a being Element of X such that
A5: ( z = a & a ref c= rng A ) ;
 z in  {  y where y is Element of X : rng A c= y ref  }  by A4, DefAtleast;
then consider b being Element of X such that
A7: ( z = b & rng A c= b ref ) ;
 ( z = a & a ref = rng A ) by A5, A7, XBOOLE_0:def_10;
then  z in  {  y where y is Element of X : y ref = rng A  }  ;
hence  z in EXACTLY A by A6, DefExactly; ::_thesis: verum
end;

theorem :: MMLQUERY:77
for n, m being Nat
for Y being ref-finite ConstructorDB
for B being FinSequence of the Constrs of Y holds EXACTLY+- (B,n,m) = (ATLEAST- (B,m)) AND (ATMOST+ (B,n))
proof
let n, m be Nat; ::_thesis: for Y being ref-finite ConstructorDB
for B being FinSequence of the Constrs of Y holds EXACTLY+- (B,n,m) = (ATLEAST- (B,m)) AND (ATMOST+ (B,n))
let Y be ref-finite ConstructorDB ; ::_thesis: for B being FinSequence of the Constrs of Y holds EXACTLY+- (B,n,m) = (ATLEAST- (B,m)) AND (ATMOST+ (B,n))
let B be FinSequence of the Constrs of Y; ::_thesis: EXACTLY+- (B,n,m) = (ATLEAST- (B,m)) AND (ATMOST+ (B,n))
thus  EXACTLY+- (B,n,m) c= (ATLEAST- (B,m)) AND (ATMOST+ (B,n)) :: according to XBOOLE_0:def_10 ::_thesis: (ATLEAST- (B,m)) AND (ATMOST+ (B,n)) c= EXACTLY+- (B,n,m)
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in EXACTLY+- (B,n,m) or z in (ATLEAST- (B,m)) AND (ATMOST+ (B,n)) )
assume A1: z in EXACTLY+- (B,n,m) ; ::_thesis: z in (ATLEAST- (B,m)) AND (ATMOST+ (B,n))
then  z in  {  x where x is Element of Y : ( card ((x ref) \ (rng B)) <= n & card ((rng B) \ (x ref)) <= m )  }  by DefExactlyPlusMinus;
then consider x being Element of Y such that
A2: ( z = x & card ((x ref) \ (rng B)) <= n & card ((rng B) \ (x ref)) <= m ) ;
 z in  {  y where y is Element of Y : card ((rng B) \ (y ref)) <= m  }  by A2;
then A3: z in ATLEAST- (B,m) by A1, DefAtleastMinus;
 z in  {  y where y is Element of Y : card ((y ref) \ (rng B)) <= n  }  by A2;
then  z in ATMOST+ (B,n) by A1, DefAtmostPlus;
hence  z in (ATLEAST- (B,m)) AND (ATMOST+ (B,n)) by A3, XBOOLE_0:def_4; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in (ATLEAST- (B,m)) AND (ATMOST+ (B,n)) or z in EXACTLY+- (B,n,m) )
assume A6: z in (ATLEAST- (B,m)) AND (ATMOST+ (B,n)) ; ::_thesis: z in EXACTLY+- (B,n,m)
then A4: ( z in ATLEAST- (B,m) & z in ATMOST+ (B,n) ) by XBOOLE_0:def_4;
then  z in  {  y where y is Element of Y : card ((y ref) \ (rng B)) <= n  }  by DefAtmostPlus;
then A5: ex y being Element of Y st
( z = y & card ((y ref) \ (rng B)) <= n ) ;
 z in  {  y where y is Element of Y : card ((rng B) \ (y ref)) <= m  }  by A4, DefAtleastMinus;
then  ex y being Element of Y st
( z = y & card ((rng B) \ (y ref)) <= m ) ;
then  z in  {  y where y is Element of Y : ( card ((y ref) \ (rng B)) <= n & card ((rng B) \ (y ref)) <= m )  }  by A5;
hence  z in EXACTLY+- (B,n,m) by A6, DefExactlyPlusMinus; ::_thesis: verum
end;

theorem Th65: :: MMLQUERY:78
for X being ConstructorDB
for A being FinSequence of the Constrs of X st A <> {} holds
ATLEAST A = meet  {  (x occur) where x is Element of X : x in rng A  }
proof
let X be ConstructorDB ; ::_thesis: for A being FinSequence of the Constrs of X st A <> {} holds
ATLEAST A = meet  {  (x occur) where x is Element of X : x in rng A  }
let A be FinSequence of the Constrs of X; ::_thesis: ( A <> {} implies ATLEAST A = meet  {  (x occur) where x is Element of X : x in rng A  }  )
assume  A <> {} ; ::_thesis: ATLEAST A = meet  {  (x occur) where x is Element of X : x in rng A  }
then  rng A <> {} by RELAT_1:41;
then consider s being set  such that
A1: s in rng A by XBOOLE_0:def_1;
 ( s in the Constrs of X & the Constrs of X c= the carrier of X ) by A1;
then reconsider s = s as Element of X ;
A2: s occur in  {  (x occur) where x is Element of X : x in rng A  }  by A1;
thus  ATLEAST A c= meet  {  (x occur) where x is Element of X : x in rng A  }  :: according to XBOOLE_0:def_10 ::_thesis: meet  {  (x occur) where x is Element of X : x in rng A  }  c= ATLEAST A
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in ATLEAST A or z in meet  {  (x occur) where x is Element of X : x in rng A  }  )
assume  z in ATLEAST A ; ::_thesis: z in meet  {  (x occur) where x is Element of X : x in rng A  }
then  z in  {  y where y is Element of X : rng A c= y ref  }  by DefAtleast;
then consider a being Element of X such that
A5: ( z = a & rng A c= a ref ) ;
now__::_thesis:_for_Y_being_set_st_Y_in__{__(x_occur)_where_x_is_Element_of_X_:_x_in_rng_A__}__holds_
z_in_Y
let Y be set ; ::_thesis: ( Y in  {  (x occur) where x is Element of X : x in rng A  }  implies z in Y )
assume  Y in  {  (x occur) where x is Element of X : x in rng A  }  ; ::_thesis: z in Y
then consider x being Element of X such that
A3: ( Y = x occur & x in rng A ) ;
thus  z in Y by A5, A3, Th10; ::_thesis: verum
end;
hence  z in meet  {  (x occur) where x is Element of X : x in rng A  }  by A2, SETFAM_1:def_1; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in meet  {  (x occur) where x is Element of X : x in rng A  }  or z in ATLEAST A )
assume A6: z in meet  {  (x occur) where x is Element of X : x in rng A  }  ; ::_thesis: z in ATLEAST A
then A8: z in s occur by A2, SETFAM_1:def_1;
then reconsider z = z as Element of X ;
 rng A c= z ref
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in rng A or s in z ref )
assume A7: s in rng A ; ::_thesis: s in z ref
then  s in the Constrs of X ;
then reconsider s = s as Element of X ;
 s occur in  {  (x occur) where x is Element of X : x in rng A  }  by A7;
then  z in s occur by A6, SETFAM_1:def_1;
hence  s in z ref by Th10; ::_thesis: verum
end;
then  z in  {  x where x is Element of X : rng A c= x ref  }  ;
hence  z in ATLEAST A by A8, DefAtleast; ::_thesis: verum
end;

theorem :: MMLQUERY:79
for X being ConstructorDB
for A being FinSequence of the Constrs of X
for c1, c2 being Element of X st A = <*c1,c2*> holds
ATLEAST A = (c1 occur) AND (c2 occur)
proof
let X be ConstructorDB ; ::_thesis: for A being FinSequence of the Constrs of X
for c1, c2 being Element of X st A = <*c1,c2*> holds
ATLEAST A = (c1 occur) AND (c2 occur)
let A be FinSequence of the Constrs of X; ::_thesis: for c1, c2 being Element of X st A = <*c1,c2*> holds
ATLEAST A = (c1 occur) AND (c2 occur)
let c1, c2 be Element of X; ::_thesis: ( A = <*c1,c2*> implies ATLEAST A = (c1 occur) AND (c2 occur) )
assume Z0: A = <*c1,c2*> ; ::_thesis: ATLEAST A = (c1 occur) AND (c2 occur)
then A0: rng A = {c1,c2} by FINSEQ_2:127;
A1:  {  (x occur) where x is Element of X : x in rng A  }  = {(c1 occur),(c2 occur)}
proof
thus   {  (x occur) where x is Element of X : x in rng A  }  c= {(c1 occur),(c2 occur)} :: according to XBOOLE_0:def_10 ::_thesis: {(c1 occur),(c2 occur)} c=  {  (x occur) where x is Element of X : x in rng A  }
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  (x occur) where x is Element of X : x in rng A  }  or z in {(c1 occur),(c2 occur)} )
assume  z in  {  (x occur) where x is Element of X : x in rng A  }  ; ::_thesis: z in {(c1 occur),(c2 occur)}
then consider x being Element of X such that
A2: ( z = x occur & x in rng A ) ;
 ( x = c1 or x = c2 ) by A0, A2, TARSKI:def_2;
hence  z in {(c1 occur),(c2 occur)} by A2, TARSKI:def_2; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in {(c1 occur),(c2 occur)} or z in  {  (x occur) where x is Element of X : x in rng A  }  )
assume  z in {(c1 occur),(c2 occur)} ; ::_thesis: z in  {  (x occur) where x is Element of X : x in rng A  }
then A3: ( z = c1 occur or z = c2 occur ) by TARSKI:def_2;
 ( c1 in rng A & c2 in rng A ) by A0, TARSKI:def_2;
hence  z in  {  (x occur) where x is Element of X : x in rng A  }  by A3; ::_thesis: verum
end;
thus  ATLEAST A = meet  {  (x occur) where x is Element of X : x in rng A  }  by Z0, Th65
.= (c1 occur) AND (c2 occur) by A1, SETFAM_1:11 ; ::_thesis: verum
end;