let L1, L2 be non empty LattStr ; :: thesis: ( LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) implies for a being Element of L1
for b being Element of L2
for X being set st a = b holds
( ( a is_less_than X implies b is_less_than X ) & ( b is_less_than X implies a is_less_than X ) & ( a is_greater_than X implies b is_greater_than X ) & ( b is_greater_than X implies a is_greater_than X ) ) )
assume A1: LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) ; :: thesis: for a being Element of L1
for b being Element of L2
for X being set st a = b holds
( ( a is_less_than X implies b is_less_than X ) & ( b is_less_than X implies a is_less_than X ) & ( a is_greater_than X implies b is_greater_than X ) & ( b is_greater_than X implies a is_greater_than X ) )
let a be Element of L1; :: thesis: for b being Element of L2
for X being set st a = b holds
( ( a is_less_than X implies b is_less_than X ) & ( b is_less_than X implies a is_less_than X ) & ( a is_greater_than X implies b is_greater_than X ) & ( b is_greater_than X implies a is_greater_than X ) )
let b be Element of L2; :: thesis: for X being set st a = b holds
( ( a is_less_than X implies b is_less_than X ) & ( b is_less_than X implies a is_less_than X ) & ( a is_greater_than X implies b is_greater_than X ) & ( b is_greater_than X implies a is_greater_than X ) )
let X be set ; :: thesis: ( a = b implies ( ( a is_less_than X implies b is_less_than X ) & ( b is_less_than X implies a is_less_than X ) & ( a is_greater_than X implies b is_greater_than X ) & ( b is_greater_than X implies a is_greater_than X ) ) )
assume A2: a = b ; :: thesis: ( ( a is_less_than X implies b is_less_than X ) & ( b is_less_than X implies a is_less_than X ) & ( a is_greater_than X implies b is_greater_than X ) & ( b is_greater_than X implies a is_greater_than X ) )
thus ( a is_less_than X implies b is_less_than X ) :: thesis: ( ( b is_less_than X implies a is_less_than X ) & ( a is_greater_than X implies b is_greater_than X ) & ( b is_greater_than X implies a is_greater_than X ) )

proof

assume A3: for c being Element of L1 st c in X holds
a [= c ; :: according to LATTICE3:def 16 :: thesis: b is_less_than X
let c be Element of L2; :: according to LATTICE3:def 16 :: thesis: ( not c in X or b [= c )
reconsider d = c as Element of L1 by A1;
assume c in X ; :: thesis: b [= c
then a [= d by A3;
hence b [= c by A1, A2; :: thesis: verum

end;

thus ( b is_less_than X implies a is_less_than X ) :: thesis: ( a is_greater_than X iff b is_greater_than X )

proof

assume A4: for c being Element of L2 st c in X holds
b [= c ; :: according to LATTICE3:def 16 :: thesis: a is_less_than X
let c be Element of L1; :: according to LATTICE3:def 16 :: thesis: ( not c in X or a [= c )
reconsider d = c as Element of L2 by A1;
assume c in X ; :: thesis: a [= c
then b [= d by A4;
hence a [= c by A1, A2; :: thesis: verum

end;

thus ( a is_greater_than X implies b is_greater_than X ) :: thesis: ( b is_greater_than X implies a is_greater_than X )

proof

assume A5: for c being Element of L1 st c in X holds
c [= a ; :: according to LATTICE3:def 17 :: thesis: b is_greater_than X
let c be Element of L2; :: according to LATTICE3:def 17 :: thesis: ( not c in X or c [= b )
reconsider d = c as Element of L1 by A1;
assume c in X ; :: thesis: c [= b
then d [= a by A5;
hence c [= b by A1, A2; :: thesis: verum

end;

assume A6: for c being Element of L2 st c in X holds
c [= b ; :: according to LATTICE3:def 17 :: thesis: a is_greater_than X
let c be Element of L1; :: according to LATTICE3:def 17 :: thesis: ( not c in X or c [= a )
reconsider d = c as Element of L2 by A1;
assume c in X ; :: thesis: c [= a
then d [= b by A6;
hence c [= a by A1, A2; :: thesis: verum