A1: "\/" (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 9 :: thesis: ( not a in { ("\/" X,F1()) where X is Subset of F1() : P1[X] } or a <= "\/" (union { X where X is Subset of F1() : P1[X] } ),F1() )
assume a in { ("\/" X,F1()) where X is Subset of F1() : P1[X] } ; :: thesis: a <= "\/" (union { X where X is Subset of F1() : P1[X] } ),F1()
then consider q being Subset of F1() such that
A2: a = "\/" q,F1() and
A3: P1[q] ;
A4: ( ex_sup_of q,F1() & ex_sup_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 A3;
hence a <= "\/" (union { X where X is Subset of F1() : P1[X] } ),F1() by A2, A4, YELLOW_0:34, ZFMISC_1:92; :: thesis: verum
end;
ex_sup_of { ("\/" X,F1()) where X is Subset of F1() : P1[X] } ,F1() by YELLOW_0:17;
hence "\/" { ("\/" X,F1()) where X is Subset of F1() : P1[X] } ,F1() <= "\/" (union { X where X is Subset of F1() : P1[X] } ),F1() by A1, YELLOW_0:def 9; :: thesis: verum