defpred S₁[ set ] means ( ( for R being strict RelStr st the carrier of R is 1 -element & 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 the carrier of R is 1 -element & 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 the carrier of R is 1 -element & 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: 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 S2 being strict RelStr such that
A5: S2 = H2 and
A6: the carrier of S2 in FinSETS by A4, Def4;
reconsider RS9 = sum_of (H1,H2) as strict RelStr ;
consider S1 being strict RelStr such that
A7: S1 = H1 and
A8: the carrier of S1 in FinSETS by A3, Def4;
reconsider RS = union_of (S1,S2) as strict RelStr ;
A9: the carrier of H1 \/ the carrier of H2 in FinSETS by A7, A8, A5, A6, CLASSES2:60;
then the carrier of RS in FinSETS by A7, A5, Def2;
hence union_of (H1,H2) in fin_RelStr by A7, A5, Def4; :: thesis: sum_of (H1,H2) in fin_RelStr
the carrier of RS9 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;

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

proof

A12: 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
A13: the carrier of H1 misses the carrier of H2 and
A14: H1 in IT and
A15: H2 in IT ; :: thesis: ( union_of (H1,H2) in IT & sum_of (H1,H2) in IT )
A16: 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 A17: Y in X ; :: thesis: sum_of (H1,H2) in Y
then A18: H2 in Y by A11, A15, SETFAM_1:def 1;
H1 in Y by A11, A14, A17, SETFAM_1:def 1;
hence sum_of (H1,H2) in Y by A1, A13, A17, A18; :: thesis: verum

end;

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: H2 in Y by A11, A15, SETFAM_1:def 1;
H1 in Y by A11, A14, A19, SETFAM_1:def 1;
hence union_of (H1,H2) in Y by A1, A13, A19, A20; :: thesis: verum

end;

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

end;

for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in IT

proof

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

end;

hence S₁[IT] by A12; :: thesis: for X being Subset of fin_RelStr st S₁[X] holds
IT c= X
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

A24: Y in X by A1, A23;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in IT or x in Y )
assume x in IT ; :: thesis: x in Y
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 the carrier of R is 1 -element & 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 the carrier of R is 1 -element & 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