A1:
"/\" { ("/\" 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();
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();
:: according to LATTICE3:def 8 :: thesis: ( 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] }
;
:: thesis: "/\" { ("/\" X,F1()) where X is Subset of F1() : P1[X] } ,F1() <= a
then consider b being
set such that A2:
(
a in b &
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 &
P1[
c] )
by A2;
A4:
"/\" c,
F1()
<= a
by A2, A3, YELLOW_2:24;
"/\" c,
F1()
in { ("/\" X,F1()) where X is Subset of F1() : P1[X] }
by A3;
then
"/\" c,
F1()
>= "/\" { ("/\" X,F1()) where X is Subset of F1() : P1[X] } ,
F1()
by YELLOW_2:24;
hence
"/\" { ("/\" X,F1()) where X is Subset of F1() : P1[X] } ,
F1()
<= a
by A4, YELLOW_0:def 2;
:: thesis: verum
end;
then
"/\" (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;
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, ORDERS_2:25; :: thesis: verum