let X be RelStr ; :: thesis: ( X in fin_RelStr_sp implies X is symmetric )
assume A1: X in fin_RelStr_sp ; :: thesis: X is symmetric
per cases ( X is trivial or not X is trivial ) ;
suppose A2: X is trivial ; :: thesis: X is symmetric
thus X is symmetric :: thesis: verum
proof
per cases ( the carrier of X is empty or ex x being object st the carrier of X = {x} ) by ;
suppose A3: the carrier of X is empty ; :: thesis: X is symmetric
let a, b be object ; :: according to NECKLACE:def 3,RELAT_2:def 3 :: thesis: ( not a in the carrier of X or not b in the carrier of X or not [a,b] in the InternalRel of X or [b,a] in the InternalRel of X )
assume that
A4: a in the carrier of X and
b in the carrier of X and
[a,b] in the InternalRel of X ; :: thesis: [b,a] in the InternalRel of X
thus [b,a] in the InternalRel of X by A3, A4; :: thesis: verum
end;
suppose ex x being object st the carrier of X = {x} ; :: thesis: X is symmetric
then consider x being object such that
A5: the carrier of X = {x} ;
A6: [: the carrier of X, the carrier of X:] = {[x,x]} by ;
thus X is symmetric :: thesis: verum
proof
per cases ( the InternalRel of X = {} or the InternalRel of X = {[x,x]} ) by ;
suppose A7: the InternalRel of X = {} ; :: thesis: X is symmetric
let a, b be object ; :: according to NECKLACE:def 3,RELAT_2:def 3 :: thesis: ( not a in the carrier of X or not b in the carrier of X or not [a,b] in the InternalRel of X or [b,a] in the InternalRel of X )
assume that
a in the carrier of X and
b in the carrier of X and
A8: [a,b] in the InternalRel of X ; :: thesis: [b,a] in the InternalRel of X
thus [b,a] in the InternalRel of X by A7, A8; :: thesis: verum
end;
suppose A9: the InternalRel of X = {[x,x]} ; :: thesis: X is symmetric
let a, b be object ; :: according to NECKLACE:def 3,RELAT_2:def 3 :: thesis: ( not a in the carrier of X or not b in the carrier of X or not [a,b] in the InternalRel of X or [b,a] in the InternalRel of X )
assume that
a in the carrier of X and
b in the carrier of X and
A10: [a,b] in the InternalRel of X ; :: thesis: [b,a] in the InternalRel of X
A11: [a,b] = [x,x] by ;
then a = x by XTUPLE_0:1;
hence [b,a] in the InternalRel of X by ; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
suppose A12: not X is trivial ; :: thesis: X is symmetric
defpred S1[ Nat] means for X being non empty RelStr st not X is trivial & X in fin_RelStr_sp & card the carrier of X c= \$1 holds
X is symmetric ;
A13: ex R being strict RelStr st
( X = R & the carrier of R in FinSETS ) by ;
reconsider X = X as non empty RelStr by ;
A14: card the carrier of X is Nat by A13;
A15: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A16: S1[k] ; :: thesis: S1[k + 1]
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
let Y be non empty RelStr ; :: thesis: ( not Y is trivial & Y in fin_RelStr_sp & card the carrier of Y c= k + 1 implies Y is symmetric )
assume that
A17: not Y is trivial and
A18: Y in fin_RelStr_sp ; :: thesis: ( not card the carrier of Y c= k + 1 or Y is symmetric )
consider H1, H2 being strict RelStr such that
A19: the carrier of H1 misses the carrier of H2 and
A20: H1 in fin_RelStr_sp and
A21: H2 in fin_RelStr_sp and
A22: ( Y = union_of (H1,H2) or Y = sum_of (H1,H2) ) by ;
ex R being strict RelStr st
( Y = R & the carrier of R in FinSETS ) by ;
then reconsider cY = the carrier of Y as finite set ;
assume card the carrier of Y c= k + 1 ; :: thesis: Y is symmetric
then Segm (card cY) c= Segm (card (k1 + 1)) ;
then card cY <= card (k1 + 1) by NAT_1:39;
then A23: card cY <= k + 1 ;
set cH1 = the carrier of H1;
set cH2 = the carrier of H2;
A24: card cY = card ( the carrier of H1 \/ the carrier of H2) by ;
ex R2 being strict RelStr st
( H2 = R2 & the carrier of R2 in FinSETS ) by ;
then reconsider cH2 = the carrier of H2 as finite set ;
ex R1 being strict RelStr st
( H1 = R1 & the carrier of R1 in FinSETS ) by ;
then reconsider cH1 = the carrier of H1 as finite set ;
A25: card cY = (card cH1) + (card cH2) by ;
not H1 is empty by ;
then A26: card cH1 >= 1 by NAT_1:14;
not H2 is empty by ;
then A27: card cH2 >= 1 by NAT_1:14;
per cases ( card cY <= k or ( card cY = k + 1 & k = 0 ) or ( (card cH1) + (card cH2) = k + 1 & k > 0 & card cH1 = 1 & card cH2 = 1 ) or ( (card cH1) + (card cH2) = k + 1 & k > 0 & card cH1 = 1 & card cH2 > 1 ) or ( (card cH1) + (card cH2) = k + 1 & k > 0 & card cH1 > 1 & card cH2 = 1 ) or ( (card cH1) + (card cH2) = k + 1 & k > 0 & card cH1 > 1 & card cH2 > 1 ) ) by ;
suppose A29: ( (card cH1) + (card cH2) = k + 1 & k > 0 & card cH1 = 1 & card cH2 = 1 ) ; :: thesis: Y is symmetric
then ex x being object st cH1 = {x} by CARD_2:42;
then the InternalRel of H1 is_symmetric_in cH1 by Th5;
then reconsider H1 = H1 as symmetric RelStr by NECKLACE:def 3;
ex y being object st cH2 = {y} by ;
then the InternalRel of H2 is_symmetric_in cH2 by Th5;
then reconsider H2 = H2 as symmetric RelStr by NECKLACE:def 3;
union_of (H1,H2) is symmetric ;
hence Y is symmetric by A22; :: thesis: verum
end;
suppose A30: ( (card cH1) + (card cH2) = k + 1 & k > 0 & card cH1 = 1 & card cH2 > 1 ) ; :: thesis: Y is symmetric
then ex x being object st cH1 = {x} by CARD_2:42;
then the InternalRel of H1 is_symmetric_in cH1 by Th5;
then reconsider H1 = H1 as symmetric RelStr by NECKLACE:def 3;
not card cH2 is trivial by ;
then card cH2 >= 2 by NAT_2:29;
then ( not H2 is empty & not H2 is trivial ) by NAT_D:60;
then reconsider H2 = H2 as symmetric RelStr by ;
union_of (H1,H2) is symmetric ;
hence Y is symmetric by A22; :: thesis: verum
end;
suppose A31: ( (card cH1) + (card cH2) = k + 1 & k > 0 & card cH1 > 1 & card cH2 = 1 ) ; :: thesis: Y is symmetric
then ex x being object st cH2 = {x} by CARD_2:42;
then the InternalRel of H2 is_symmetric_in cH2 by Th5;
then reconsider H2 = H2 as symmetric RelStr by NECKLACE:def 3;
not card cH1 is trivial by ;
then card cH1 >= 2 by NAT_2:29;
then ( not H1 is empty & not H1 is trivial ) by NAT_D:60;
then reconsider H1 = H1 as symmetric RelStr by ;
union_of (H1,H2) is symmetric ;
hence Y is symmetric by A22; :: thesis: verum
end;
suppose A32: ( (card cH1) + (card cH2) = k + 1 & k > 0 & card cH1 > 1 & card cH2 > 1 ) ; :: thesis: Y is symmetric
then not card cH2 is trivial by NAT_2:28;
then card cH2 >= 2 by NAT_2:29;
then A33: ( not H2 is empty & not H2 is trivial ) by NAT_D:60;
card cH2 < k + 1
proof
assume not card cH2 < k + 1 ; :: thesis: contradiction
then (card cH1) + (card cH2) >= (k + 1) + 1 by ;
hence contradiction by A32, NAT_1:13; :: thesis: verum
end;
then card cH2 <= k by NAT_1:13;
then card cH2 <= card k1 ;
then Segm (card cH2) c= Segm (card k) by NAT_1:39;
then card cH2 c= k1 ;
then reconsider H2 = H2 as symmetric RelStr by ;
not card cH1 is trivial by ;
then card cH1 >= 2 by NAT_2:29;
then A34: ( not H1 is empty & not H1 is trivial ) by NAT_D:60;
card cH1 < k + 1
proof
assume not card cH1 < k + 1 ; :: thesis: contradiction
then (card cH1) + (card cH2) >= (k + 1) + 1 by ;
hence contradiction by A32, NAT_1:13; :: thesis: verum
end;
then card cH1 <= k by NAT_1:13;
then card cH1 <= card k1 ;
then Segm (card cH1) c= Segm (card k) by NAT_1:39;
then card cH1 c= k1 ;
then reconsider H1 = H1 as symmetric RelStr by ;
union_of (H1,H2) is symmetric ;
hence Y is symmetric by A22; :: thesis: verum
end;
end;
end;
A35: S1[ 0 ] ;
for k being Nat holds S1[k] from hence X is symmetric by A1, A12, A14; :: thesis: verum
end;
end;