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