let X be set ; :: thesis: ( X in fin_RelStr_sp implies X is non empty finite strict RelStr )

assume A1: X in fin_RelStr_sp ; :: thesis: X is non empty finite strict RelStr

then A2: ex R being strict RelStr st

( X = R & the carrier of R in FinSETS ) by Def4;

then reconsider R = X as strict RelStr ;

assume A1: X in fin_RelStr_sp ; :: thesis: X is non empty finite strict RelStr

then A2: ex R being strict RelStr st

( X = R & the carrier of R in FinSETS ) by Def4;

then reconsider R = X as strict RelStr ;

now :: thesis: not R is empty

hence
X is non empty finite strict RelStr
by A2; :: thesis: verumset M = fin_RelStr_sp \ {R};

set F = fin_RelStr_sp ;

reconsider M = fin_RelStr_sp \ {R} as Subset of fin_RelStr ;

A3: R in {R} by TARSKI:def 1;

assume A4: R is empty ; :: thesis: contradiction

hence contradiction by A1, A3, XBOOLE_0:def 5; :: thesis: verum

end;set F = fin_RelStr_sp ;

reconsider M = fin_RelStr_sp \ {R} as Subset of fin_RelStr ;

A3: R in {R} by TARSKI:def 1;

assume A4: R is empty ; :: thesis: contradiction

A5: now :: thesis: 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 )

( union_of (H1,H2) in M & sum_of (H1,H2) in M )

let H1, H2 be strict RelStr ; :: thesis: ( the carrier of H1 misses the carrier of H2 & H1 in M & H2 in M implies ( union_of (H1,H2) in M & sum_of (H1,H2) in M ) )

assume that

A6: the carrier of H1 misses the carrier of H2 and

A7: H1 in M and

A8: H2 in M ; :: thesis: ( union_of (H1,H2) in M & sum_of (H1,H2) in M )

A9: H2 in fin_RelStr_sp by A8, XBOOLE_0:def 5;

A10: not H1 in {R} by A7, XBOOLE_0:def 5;

the carrier of H1 <> {}

A \/ the carrier of H2 <> {} ;

then union_of (H1,H2) <> R by A4, Def2;

then A12: not union_of (H1,H2) in {R} by TARSKI:def 1;

the carrier of (sum_of (H1,H2)) = A \/ the carrier of H2 by Def3;

then A13: not sum_of (H1,H2) in {R} by A4, TARSKI:def 1;

A14: H1 in fin_RelStr_sp by A7, XBOOLE_0:def 5;

then union_of (H1,H2) in fin_RelStr_sp by A6, A9, Def5;

hence union_of (H1,H2) in M by A12, XBOOLE_0:def 5; :: thesis: sum_of (H1,H2) in M

sum_of (H1,H2) in fin_RelStr_sp by A6, A14, A9, Def5;

hence sum_of (H1,H2) in M by A13, XBOOLE_0:def 5; :: thesis: verum

end;assume that

A6: the carrier of H1 misses the carrier of H2 and

A7: H1 in M and

A8: H2 in M ; :: thesis: ( union_of (H1,H2) in M & sum_of (H1,H2) in M )

A9: H2 in fin_RelStr_sp by A8, XBOOLE_0:def 5;

A10: not H1 in {R} by A7, XBOOLE_0:def 5;

the carrier of H1 <> {}

proof
end;

then reconsider A = the carrier of H1 as non empty set ;per cases
( the carrier of H1 <> the carrier of R or the InternalRel of H1 <> the InternalRel of R )
by A10, TARSKI:def 1;

end;

suppose A11:
the InternalRel of H1 <> the InternalRel of R
; :: thesis: the carrier of H1 <> {}

set InterH1 = the InternalRel of H1;

the InternalRel of H1 <> {} by A4, A11;

hence the carrier of H1 <> {} ; :: thesis: verum

end;the InternalRel of H1 <> {} by A4, A11;

hence the carrier of H1 <> {} ; :: thesis: verum

A \/ the carrier of H2 <> {} ;

then union_of (H1,H2) <> R by A4, Def2;

then A12: not union_of (H1,H2) in {R} by TARSKI:def 1;

the carrier of (sum_of (H1,H2)) = A \/ the carrier of H2 by Def3;

then A13: not sum_of (H1,H2) in {R} by A4, TARSKI:def 1;

A14: H1 in fin_RelStr_sp by A7, XBOOLE_0:def 5;

then union_of (H1,H2) in fin_RelStr_sp by A6, A9, Def5;

hence union_of (H1,H2) in M by A12, XBOOLE_0:def 5; :: thesis: sum_of (H1,H2) in M

sum_of (H1,H2) in fin_RelStr_sp by A6, A14, A9, Def5;

hence sum_of (H1,H2) in M by A13, XBOOLE_0:def 5; :: thesis: verum

now :: thesis: for S being strict RelStr st the carrier of S is 1 -element & the carrier of S in FinSETS holds

S in M

then
fin_RelStr_sp c= M
by A5, Def5;S in M

let S be strict RelStr ; :: thesis: ( the carrier of S is 1 -element & the carrier of S in FinSETS implies S in M )

assume that

A15: the carrier of S is 1 -element and

A16: the carrier of S in FinSETS ; :: thesis: S in M

A17: not S in {R} by A4, A15, TARSKI:def 1;

S in fin_RelStr_sp by A15, A16, Def5;

hence S in M by A17, XBOOLE_0:def 5; :: thesis: verum

end;assume that

A15: the carrier of S is 1 -element and

A16: the carrier of S in FinSETS ; :: thesis: S in M

A17: not S in {R} by A4, A15, TARSKI:def 1;

S in fin_RelStr_sp by A15, A16, Def5;

hence S in M by A17, XBOOLE_0:def 5; :: thesis: verum

hence contradiction by A1, A3, XBOOLE_0:def 5; :: thesis: verum