defpred S₁[ set ] means ( ( for R being strict RelStr st not the carrier of R is empty & the carrier of R is trivial & the carrier of R in FinSETS holds
R in $1 ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in $1 & H2 in $1 holds
( union_of H1,H2 in $1 & sum_of H1,H2 in $1 ) ) );
consider X being set such that
A1: for x being set holds
( x in X iff ( x in bool fin_RelStr & S₁[x] ) ) from XBOOLE_0:sch 1();
for x being set st x in X holds
x in bool fin_RelStr by A1;
then reconsider X = X as Subset-Family of fin_RelStr by TARSKI:def 3;
take IT = Intersect X; :: thesis: ( ( for R being strict RelStr st not the carrier of R is empty & the carrier of R is trivial & the carrier of R in FinSETS holds
R in IT ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in IT & H2 in IT holds
( union_of H1,H2 in IT & sum_of H1,H2 in IT ) ) & ( for M being Subset of fin_RelStr st ( for R being strict RelStr st not the carrier of R is empty & the carrier of R is trivial & the carrier of R in FinSETS holds
R in M ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in M & H2 in M holds
( union_of H1,H2 in M & sum_of H1,H2 in M ) ) holds
IT c= M ) )
A2: fin_RelStr in bool fin_RelStr by ZFMISC_1:def 1;
S₁[ fin_RelStr ]

proof

set A = fin_RelStr ;
for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr & H2 in fin_RelStr holds
( union_of H1,H2 in fin_RelStr & sum_of H1,H2 in fin_RelStr )

proof

let H1, H2 be strict RelStr ; :: thesis: ( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr & H2 in fin_RelStr implies ( union_of H1,H2 in fin_RelStr & sum_of H1,H2 in fin_RelStr ) )
assume that
the carrier of H1 misses the carrier of H2 and
A3: H1 in fin_RelStr and
A4: H2 in fin_RelStr ; :: thesis: ( union_of H1,H2 in fin_RelStr & sum_of H1,H2 in fin_RelStr )
consider S1 being strict RelStr such that
A5: S1 = H1 and
A6: the carrier of S1 in FinSETS by A3, Def4;
consider S2 being strict RelStr such that
A7: S2 = H2 and
A8: the carrier of S2 in FinSETS by A4, Def4;
A9: the carrier of H1 \/ the carrier of H2 in FinSETS by A5, A6, A7, A8, CLASSES2:66;
reconsider RS = union_of S1,S2 as strict RelStr ;
the carrier of RS in FinSETS by A5, A7, A9, Def2;
hence union_of H1,H2 in fin_RelStr by A5, A7, Def4; :: thesis: sum_of H1,H2 in fin_RelStr
reconsider RS' = sum_of H1,H2 as strict RelStr ;
the carrier of RS' in FinSETS by A9, Def3;
hence sum_of H1,H2 in fin_RelStr by Def4; :: thesis: verum

end;

hence S₁[ fin_RelStr ] by Def4; :: thesis: verum

end;

then A10: X <> {} by A1, A2;
then A11: IT = meet X by SETFAM_1:def 10;
( S₁[IT] & ( for X being Subset of fin_RelStr st S₁[X] holds
IT c= X ) )

proof

thus S₁[IT] :: thesis: for X being Subset of fin_RelStr st S₁[X] holds
IT c= X

proof

A12: for R being strict RelStr st not the carrier of R is empty & the carrier of R is trivial & the carrier of R in FinSETS holds
R in IT

proof

let R be strict RelStr ; :: thesis: ( not the carrier of R is empty & the carrier of R is trivial & the carrier of R in FinSETS implies R in IT )
assume that
A13: ( not the carrier of R is empty & the carrier of R is trivial ) and
A14: the carrier of R in FinSETS ; :: thesis: R in IT
for Y being set st Y in X holds
R in Y by A1, A13, A14;
hence R in IT by A10, A11, SETFAM_1:def 1; :: thesis: verum

end;

for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in IT & H2 in IT holds
( union_of H1,H2 in IT & sum_of H1,H2 in IT )

proof

let H1, H2 be strict RelStr ; :: thesis: ( the carrier of H1 misses the carrier of H2 & H1 in IT & H2 in IT implies ( union_of H1,H2 in IT & sum_of H1,H2 in IT ) )
assume that
A15: the carrier of H1 misses the carrier of H2 and
A16: H1 in IT and
A17: H2 in IT ; :: thesis: ( union_of H1,H2 in IT & sum_of H1,H2 in IT )
A18: for Y being set st Y in X holds
union_of H1,H2 in Y

proof

let Y be set ; :: thesis: ( Y in X implies union_of H1,H2 in Y )
assume A19: Y in X ; :: thesis: union_of H1,H2 in Y
then A20: H1 in Y by A11, A16, SETFAM_1:def 1;
H2 in Y by A11, A17, A19, SETFAM_1:def 1;
hence union_of H1,H2 in Y by A1, A15, A19, A20; :: thesis: verum

end;

sum_of H1,H2 in IT

proof

for Y being set st Y in X holds
sum_of H1,H2 in Y

proof

let Y be set ; :: thesis: ( Y in X implies sum_of H1,H2 in Y )
assume A21: Y in X ; :: thesis: sum_of H1,H2 in Y
then A22: H1 in Y by A11, A16, SETFAM_1:def 1;
H2 in Y by A11, A17, A21, SETFAM_1:def 1;
hence sum_of H1,H2 in Y by A1, A15, A21, A22; :: thesis: verum

end;

hence sum_of H1,H2 in IT by A10, A11, SETFAM_1:def 1; :: thesis: verum

end;

hence ( union_of H1,H2 in IT & sum_of H1,H2 in IT ) by A10, A11, A18, SETFAM_1:def 1; :: thesis: verum

end;

hence S₁[IT] by A12; :: thesis: verum

end;

let Y be Subset of fin_RelStr ; :: thesis: ( S₁[Y] implies IT c= Y )
assume A23: S₁[Y] ; :: thesis: IT c= Y
IT c= Y

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in IT or x in Y )
assume A24: x in IT ; :: thesis: x in Y
Y in X by A1, A23;
hence x in Y by A11, A24, SETFAM_1:def 1; :: thesis: verum

end;

hence IT c= Y ; :: thesis: verum

end;

hence ( ( for R being strict RelStr st not the carrier of R is empty & the carrier of R is trivial & the carrier of R in FinSETS holds
R in IT ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in IT & H2 in IT holds
( union_of H1,H2 in IT & sum_of H1,H2 in IT ) ) & ( for M being Subset of fin_RelStr st ( for R being strict RelStr st not the carrier of R is empty & the carrier of R is trivial & the carrier of R in FinSETS holds
R in M ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in M & H2 in M holds
( union_of H1,H2 in M & sum_of H1,H2 in M ) ) holds
IT c= M ) ) ; :: thesis: verum