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 ) )

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

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

thus
( b is_less_than X implies a is_less_than X )
:: thesis: ( a is_greater_than X iff b is_greater_than X )
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;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

proof

thus
( a is_greater_than X implies b is_greater_than X )
:: thesis: ( b is_greater_than X implies a is_greater_than X )
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;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

proof

assume A6:
for c being Element of L2 st c in X holds
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;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

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