union { X where X is Subset of F1() : P1[X] } is_>=_than "/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1())
proof
let a be
Element of
F1();
LATTICE3:def 8 ( not a in union { X where X is Subset of F1() : P1[X] } or "/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) <= a )
assume
a in union { X where X is Subset of F1() : P1[X] }
;
"/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) <= a
then consider b being
set such that A1:
a in b
and A2:
b in { X where X is Subset of F1() : P1[X] }
by TARSKI:def 4;
consider c being
Subset of
F1()
such that A3:
b = c
and A4:
P1[
c]
by A2;
"/\" (
c,
F1())
in { ("/\" (X,F1())) where X is Subset of F1() : P1[X] }
by A4;
then A5:
"/\" (
c,
F1())
>= "/\" (
{ ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,
F1())
by YELLOW_2:22;
"/\" (
c,
F1())
<= a
by A1, A3, YELLOW_2:22;
hence
"/\" (
{ ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,
F1())
<= a
by A5, YELLOW_0:def 2;
verum
end;
then A6:
"/\" ((union { X where X is Subset of F1() : P1[X] } ),F1()) >= "/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1())
by YELLOW_0:33;
"/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) >= "/\" ((union { X where X is Subset of F1() : P1[X] } ),F1())
from YELLOW_3:sch 2();
hence
"/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) = "/\" ((union { X where X is Subset of F1() : P1[X] } ),F1())
by A6, ORDERS_2:2; verum