"/\" ((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();
LATTICE3:def 8 ( 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] }
;
"/\" ((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;
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; verum