A1:
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 9 ( not a in union { X where X is Subset of F1() : P1[X] } or a <= "\/" ( { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) )
assume
a in union { X where X is Subset of F1() : P1[X] }
;
a <= "\/" ( { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } ,F1())
then consider b being
set such that A2:
a in b
and A3:
b in { X where X is Subset of F1() : P1[X] }
by TARSKI:def 4;
consider c being
Subset of
F1()
such that A4:
b = c
and A5:
P1[
c]
by A3;
"\/" (
c,
F1())
in { ("\/" (X,F1())) where X is Subset of F1() : P1[X] }
by A5;
then A6:
"\/" (
c,
F1())
<= "\/" (
{ ("\/" (X,F1())) where X is Subset of F1() : P1[X] } ,
F1())
by YELLOW_2:22;
a <= "\/" (
c,
F1())
by A2, A4, YELLOW_2:22;
hence
a <= "\/" (
{ ("\/" (X,F1())) where X is Subset of F1() : P1[X] } ,
F1())
by A6, YELLOW_0:def 2;
verum
end;
A7:
"\/" ( { ("\/" (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 4();
ex_sup_of union { X where X is Subset of F1() : P1[X] } ,F1()
by YELLOW_0:17;
then
"\/" ((union { X where X is Subset of F1() : P1[X] } ),F1()) <= "\/" ( { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } ,F1())
by A1, YELLOW_0:def 9;
hence
"\/" ( { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) = "\/" ((union { X where X is Subset of F1() : P1[X] } ),F1())
by A7, ORDERS_2:2; verum