let M be Matrix of 3,F_Real; :: thesis: lines M = {(Line (M,1)),(Line (M,2)),(Line (M,3))}
A1: lines M c= {(Line (M,1)),(Line (M,2)),(Line (M,3))}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in lines M or x in {(Line (M,1)),(Line (M,2)),(Line (M,3))} )
assume x in lines M ; :: thesis: x in {(Line (M,1)),(Line (M,2)),(Line (M,3))}
then consider i being Nat such that
A2: i in Seg 3 and
A3: x = Line (M,i) by MATRIX13:103;
( i = 1 or i = 2 or i = 3 ) by A2, FINSEQ_3:1, ENUMSET1:def 1;
hence x in {(Line (M,1)),(Line (M,2)),(Line (M,3))} by A3, ENUMSET1:def 1; :: thesis: verum
end;
{(Line (M,1)),(Line (M,2)),(Line (M,3))} c= lines M
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(Line (M,1)),(Line (M,2)),(Line (M,3))} or x in lines M )
assume x in {(Line (M,1)),(Line (M,2)),(Line (M,3))} ; :: thesis: x in lines M
then A4: ( x = Line (M,1) or x = Line (M,2) or x = Line (M,3) ) by ENUMSET1:def 1;
( 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 ) by FINSEQ_1:1;
hence x in lines M by A4, MATRIX13:103; :: thesis: verum
end;
hence lines M = {(Line (M,1)),(Line (M,2)),(Line (M,3))} by A1; :: thesis: verum