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 8 :: thesis: ( not a in union { X where X is Subset of F1() : P1[X] } or "/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) <= a )
assume a in union { X where X is Subset of F1() : P1[X] } ; :: thesis: "/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) <= a
then consider b being set such that
A1: a in b and
A2: b in { X where X is Subset of F1() : P1[X] } by TARSKI:def 4;
consider c being Subset of F1() such that
A3: b = c and
A4: P1[c] by A2;
"/\" (c,F1()) in { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } by A4;
then A5: "/\" (c,F1()) >= "/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) by YELLOW_2:24;
"/\" (c,F1()) <= a by A1, A3, YELLOW_2:24;
hence "/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) <= a by A5, YELLOW_0:def 2; :: thesis: verum
end;
then A6: "/\" ((union { X where X is Subset of F1() : P1[X] } ),F1()) >= "/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) by YELLOW_0:33;
"/\" ( { ("/\" (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 2();
 hence "/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) = "/\" ((union { X where X is Subset of F1() : P1[X] } ),F1()) by A6, ORDERS_2:25; :: thesis: verum