"/\" ((union { X where X is Subset of F1() : P1[X] } ),F1()) is_<=_than { ("/\" (X,F1())) where X is Subset of F1() : P1[X] }
proof
let a be Element of F1(); :: according to LATTICE3:def 8 :: thesis: ( not a in { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } or "/\" ((union { X where X is Subset of F1() : P1[X] } ),F1()) <= a )
assume a in { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ; :: thesis: "/\" ((union { X where X is Subset of F1() : P1[X] } ),F1()) <= a
then consider q being Subset of F1() such that
A1: a = "/\" (q,F1()) and
A2: P1[q] ;
A3: ( ex_inf_of q,F1() & ex_inf_of union { X where X is Subset of F1() : P1[X] } ,F1() ) by YELLOW_0:17;
q in { X where X is Subset of F1() : P1[X] } by A2;
hence "/\" ((union { X where X is Subset of F1() : P1[X] } ),F1()) <= a by A1, A3, YELLOW_0:35, ZFMISC_1:74; :: thesis: verum
end;
hence "/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) >= "/\" ((union { X where X is Subset of F1() : P1[X] } ),F1()) by YELLOW_0:33; :: thesis: verum