thus ( AS is Fanoian implies for a, b, c, d being Element of AS st a,b // c,d & a,c // b,d & a,d // b,c holds
a,b // a,c ) :: thesis: ( ( for a, b, c, d being Element of AS st a,b // c,d & a,c // b,d & a,d // b,c holds
a,b // a,c ) implies AS is Fanoian )
proof
assume A1: for a, b, c, d being Element of AS st a,b // c,d & a,c // b,d & a,d // b,c holds
LIN a,b,c ; :: according to TRANSLAC:def 1 :: thesis: for a, b, c, d being Element of AS st a,b // c,d & a,c // b,d & a,d // b,c holds
a,b // a,c
let a, b, c, d be Element of AS; :: thesis: ( a,b // c,d & a,c // b,d & a,d // b,c implies a,b // a,c )
assume ( a,b // c,d & a,c // b,d & a,d // b,c ) ; :: thesis: a,b // a,c
then LIN a,b,c by A1;
hence a,b // a,c by AFF_1:def 1; :: thesis: verum
end;
assume A2: for a, b, c, d being Element of AS st a,b // c,d & a,c // b,d & a,d // b,c holds
a,b // a,c ; :: thesis: AS is Fanoian
let a, b, c, d be Element of AS; :: according to TRANSLAC:def 1 :: thesis: ( not a,b // c,d or not a,c // b,d or not a,d // b,c or LIN a,b,c )
assume ( a,b // c,d & a,c // b,d & a,d // b,c ) ; :: thesis: LIN a,b,c
then a,b // a,c by A2;
hence LIN a,b,c by AFF_1:def 1; :: thesis: verum