"/\" (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:92; :: 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