set Q = F_{1}();

set X = F_{3}();

set Y = F_{4}();

set Z = { { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } where a is Element of F_{1}() : a in F_{3}() } ;

set W = { ("\/" V) where V is Subset of F_{1}() : V in { { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } where a is Element of F_{1}() : a in F_{3}() } } ;

set S = { F_{2}(a,b) where a, b is Element of F_{1}() : ( a in F_{3}() & b in F_{4}() ) } ;

A1: { ("\/" V) where V is Subset of F_{1}() : V in { { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } where a is Element of F_{1}() : a in F_{3}() } } = { ("\/" ( { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } ,F_{1}())) where a is Element of F_{1}() : a in F_{3}() }
_{2}(a,b) where a, b is Element of F_{1}() : ( a in F_{3}() & b in F_{4}() ) } = union { { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } where a is Element of F_{1}() : a in F_{3}() }
_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } where a is Element of F_{1}() : a in F_{3}() } c= bool H_{1}(F_{1}())
_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } ,F_{1}())) where a is Element of F_{1}() : a in F_{3}() } ,F_{1}()) = "\/" ( { F_{2}(a,b) where a, b is Element of F_{1}() : ( a in F_{3}() & b in F_{4}() ) } ,F_{1}())
by A1, A7, LATTICE3:48; :: thesis: verum

set X = F

set Y = F

set Z = { { F

set W = { ("\/" V) where V is Subset of F

set S = { F

A1: { ("\/" V) where V is Subset of F

proof

A7:
{ F
thus
{ ("\/" V) where V is Subset of F_{1}() : V in { { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } where a is Element of F_{1}() : a in F_{3}() } } c= { ("\/" ( { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } ,F_{1}())) where a is Element of F_{1}() : a in F_{3}() }
:: according to XBOOLE_0:def 10 :: thesis: { ("\/" ( { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } ,F_{1}())) where a is Element of F_{1}() : a in F_{3}() } c= { ("\/" V) where V is Subset of F_{1}() : V in { { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } where a is Element of F_{1}() : a in F_{3}() } } _{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } ,F_{1}())) where a is Element of F_{1}() : a in F_{3}() } or x in { ("\/" V) where V is Subset of F_{1}() : V in { { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } where a is Element of F_{1}() : a in F_{3}() } } )

assume x in { ("\/" ( { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } ,F_{1}())) where a is Element of F_{1}() : a in F_{3}() }
; :: thesis: x in { ("\/" V) where V is Subset of F_{1}() : V in { { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } where a is Element of F_{1}() : a in F_{3}() } }

then consider a being Element of F_{1}() such that

A4: x = "\/" ( { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } ,F_{1}())
and

A5: a in F_{3}()
;

A6: { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } c= H_{1}(F_{1}())
_{2}(a,c) where c is Element of F_{1}() : c in F_{4}() } in { { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } where a is Element of F_{1}() : a in F_{3}() }
by A5;

hence x in { ("\/" V) where V is Subset of F_{1}() : V in { { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } where a is Element of F_{1}() : a in F_{3}() } }
by A4, A6; :: thesis: verum

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ("\/" ( { F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ("\/" V) where V is Subset of F_{1}() : V in { { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } where a is Element of F_{1}() : a in F_{3}() } } or x in { ("\/" ( { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } ,F_{1}())) where a is Element of F_{1}() : a in F_{3}() } )

assume x in { ("\/" V) where V is Subset of F_{1}() : V in { { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } where a is Element of F_{1}() : a in F_{3}() } }
; :: thesis: x in { ("\/" ( { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } ,F_{1}())) where a is Element of F_{1}() : a in F_{3}() }

then consider V being Subset of F_{1}() such that

A2: x = "\/" V and

A3: V in { { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } where a is Element of F_{1}() : a in F_{3}() }
;

ex a being Element of F_{1}() st

( V = { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } & a in F_{3}() )
by A3;

hence x in { ("\/" ( { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } ,F_{1}())) where a is Element of F_{1}() : a in F_{3}() }
by A2; :: thesis: verum

end;assume x in { ("\/" V) where V is Subset of F

then consider V being Subset of F

A2: x = "\/" V and

A3: V in { { F

ex a being Element of F

( V = { F

hence x in { ("\/" ( { F

assume x in { ("\/" ( { F

then consider a being Element of F

A4: x = "\/" ( { F

A5: a in F

A6: { F

proof

{ F
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } or y in H_{1}(F_{1}()) )

assume y in { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() }
; :: thesis: y in H_{1}(F_{1}())

then ex b being Element of F_{1}() st

( y = F_{2}(a,b) & b in F_{4}() )
;

hence y in H_{1}(F_{1}())
; :: thesis: verum

end;assume y in { F

then ex b being Element of F

( y = F

hence y in H

hence x in { ("\/" V) where V is Subset of F

proof

{ { F
thus
{ F_{2}(a,b) where a, b is Element of F_{1}() : ( a in F_{3}() & b in F_{4}() ) } c= union { { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } where a is Element of F_{1}() : a in F_{3}() }
:: according to XBOOLE_0:def 10 :: thesis: union { { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } where a is Element of F_{1}() : a in F_{3}() } c= { F_{2}(a,b) where a, b is Element of F_{1}() : ( a in F_{3}() & b in F_{4}() ) } _{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } where a is Element of F_{1}() : a in F_{3}() } or x in { F_{2}(a,b) where a, b is Element of F_{1}() : ( a in F_{3}() & b in F_{4}() ) } )

assume x in union { { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } where a is Element of F_{1}() : a in F_{3}() }
; :: thesis: x in { F_{2}(a,b) where a, b is Element of F_{1}() : ( a in F_{3}() & b in F_{4}() ) }

then consider V being set such that

A9: x in V and

A10: V in { { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } where a is Element of F_{1}() : a in F_{3}() }
by TARSKI:def 4;

consider a being Element of F_{1}() such that

A11: V = { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() }
and

A12: a in F_{3}()
by A10;

ex b being Element of F_{1}() st

( x = F_{2}(a,b) & b in F_{4}() )
by A9, A11;

hence x in { F_{2}(a,b) where a, b is Element of F_{1}() : ( a in F_{3}() & b in F_{4}() ) }
by A12; :: thesis: verum

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union { { F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F_{2}(a,b) where a, b is Element of F_{1}() : ( a in F_{3}() & b in F_{4}() ) } or x in union { { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } where a is Element of F_{1}() : a in F_{3}() } )

assume x in { F_{2}(a,b) where a, b is Element of F_{1}() : ( a in F_{3}() & b in F_{4}() ) }
; :: thesis: x in union { { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } where a is Element of F_{1}() : a in F_{3}() }

then consider a, b being Element of F_{1}() such that

A8: ( x = F_{2}(a,b) & a in F_{3}() & b in F_{4}() )
;

( x in { F_{2}(a,c) where c is Element of F_{1}() : c in F_{4}() } & { F_{2}(a,d) where d is Element of F_{1}() : d in F_{4}() } in { { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } where a is Element of F_{1}() : a in F_{3}() } )
by A8;

hence x in union { { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } where a is Element of F_{1}() : a in F_{3}() }
by TARSKI:def 4; :: thesis: verum

end;assume x in { F

then consider a, b being Element of F

A8: ( x = F

( x in { F

hence x in union { { F

assume x in union { { F

then consider V being set such that

A9: x in V and

A10: V in { { F

consider a being Element of F

A11: V = { F

A12: a in F

ex b being Element of F

( x = F

hence x in { F

proof

hence
"\/" ( { ("\/" ( { F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } where a is Element of F_{1}() : a in F_{3}() } or x in bool H_{1}(F_{1}()) )

reconsider xx = x as set by TARSKI:1;

assume x in { { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() } where a is Element of F_{1}() : a in F_{3}() }
; :: thesis: x in bool H_{1}(F_{1}())

then consider a being Element of F_{1}() such that

A13: x = { F_{2}(a,b) where b is Element of F_{1}() : b in F_{4}() }
and

a in F_{3}()
;

xx c= H_{1}(F_{1}())
_{1}(F_{1}())
; :: thesis: verum

end;reconsider xx = x as set by TARSKI:1;

assume x in { { F

then consider a being Element of F

A13: x = { F

a in F

xx c= H

proof

hence
x in bool H
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in xx or y in H_{1}(F_{1}()) )

assume y in xx ; :: thesis: y in H_{1}(F_{1}())

then ex b being Element of F_{1}() st

( y = F_{2}(a,b) & b in F_{4}() )
by A13;

hence y in H_{1}(F_{1}())
; :: thesis: verum

end;assume y in xx ; :: thesis: y in H

then ex b being Element of F

( y = F

hence y in H