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 ;

now :: thesis: not R is empty

set 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

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 )

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 <> {}

proof

per cases ( the carrier of H1 <> the carrier of R or the InternalRel of H1 <> the InternalRel of R ) by A10, TARSKI:def 1;

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

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

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;

end;

end;

then reconsider A = the carrier of H1 as non empty set ;
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;

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

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;

then fin_RelStr_sp c= M by A5, Def5;
hence contradiction by A1, A3, XBOOLE_0:def 5; :: thesis: verum

end;

hence X is non empty finite strict RelStr by A2; :: thesis: verum