defpred S_{1}[ 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_{1}[x] ) )
from XFAMILY:sch 1();

for x being object 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_{1}[ fin_RelStr ]

then A10: X <> {} by A1, A2;

then A11: IT = meet X by SETFAM_1:def 9;

( S_{1}[IT] & ( for X being Subset of fin_RelStr st S_{1}[X] holds

IT c= X ) )

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

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

for x being object 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

proof

fin_RelStr in bool fin_RelStr
by ZFMISC_1:def 1;
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 )_{1}[ fin_RelStr ]
by Def4; :: thesis: verum

end;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

hence
S
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;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

then A10: X <> {} by A1, A2;

then A11: IT = meet X by SETFAM_1:def 9;

( S

IT c= X ) )

proof

hence
( ( for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
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 )

R in IT_{1}[IT]
by A12; :: thesis: for X being Subset of fin_RelStr st S_{1}[X] holds

IT c= X

let Y be Subset of fin_RelStr; :: thesis: ( S_{1}[Y] implies IT c= Y )

assume A23: S_{1}[Y]
; :: thesis: IT c= Y

IT c= Y

end;( union_of (H1,H2) in IT & sum_of (H1,H2) in IT )

proof

for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
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

union_of (H1,H2) in Y

end;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

for Y being set st Y in X holds
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;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

union_of (H1,H2) in Y

proof

hence
( union_of (H1,H2) in IT & sum_of (H1,H2) in IT )
by A10, A11, A16, SETFAM_1:def 1; :: thesis: verum
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;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

R in IT

proof

hence
S
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;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

IT c= X

let Y be Subset of fin_RelStr; :: thesis: ( S

assume A23: S

IT c= Y

proof

hence
IT c= Y
; :: thesis: verum
A24:
Y in X
by A1, A23;

let x be object ; :: 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;let x be object ; :: 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

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