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