A1: union { X where X is Subset of F1() : P1[X] } is_<=_than "\/" { ("\/" X,F1()) where X is Subset of F1() : P1[X] } ,F1()
proof
let a be Element of F1(); :: according to LATTICE3:def 9 :: thesis: ( not a in union { X where X is Subset of F1() : P1[X] } or a <= "\/" { ("\/" X,F1()) where X is Subset of F1() : P1[X] } ,F1() )
assume a in union { X where X is Subset of F1() : P1[X] } ; :: thesis: a <= "\/" { ("\/" X,F1()) where X is Subset of F1() : P1[X] } ,F1()
then consider b being set such that
A2: a in b and
A3: b in { X where X is Subset of F1() : P1[X] } by TARSKI:def 4;
consider c being Subset of F1() such that
A4: b = c and
A5: P1[c] by A3;
"\/" c,F1() in { ("\/" X,F1()) where X is Subset of F1() : P1[X] } by A5;
then A6: "\/" c,F1() <= "\/" { ("\/" X,F1()) where X is Subset of F1() : P1[X] } ,F1() by YELLOW_2:24;
a <= "\/" c,F1() by A2, A4, YELLOW_2:24;
hence a <= "\/" { ("\/" X,F1()) where X is Subset of F1() : P1[X] } ,F1() by A6, YELLOW_0:def 2; :: thesis: verum
end;
A7: "\/" { ("\/" X,F1()) where X is Subset of F1() : P1[X] } ,F1() <= "\/" (union { X where X is Subset of F1() : P1[X] } ),F1() from YELLOW_3:sch 4();
 ex_sup_of union { X where X is Subset of F1() : P1[X] } ,F1() by YELLOW_0:17;
then "\/" (union { X where X is Subset of F1() : P1[X] } ),F1() <= "\/" { ("\/" X,F1()) where X is Subset of F1() : P1[X] } ,F1() by A1, YELLOW_0:def 9;
hence "\/" { ("\/" X,F1()) where X is Subset of F1() : P1[X] } ,F1() = "\/" (union { X where X is Subset of F1() : P1[X] } ),F1() by A7, ORDERS_2:25; :: thesis: verum