let L be Lattice; :: thesis: for L' being SubLattice of L
for X being Subset of L'
for a being Element of L
for a' being Element of L' st a = a' holds
( a is_less_than X iff a' is_less_than X )
let L' be SubLattice of L; :: thesis: for X being Subset of L'
for a being Element of L
for a' being Element of L' st a = a' holds
( a is_less_than X iff a' is_less_than X )
let X be Subset of L'; :: thesis: for a being Element of L
for a' being Element of L' st a = a' holds
( a is_less_than X iff a' is_less_than X )
let a be Element of L; :: thesis: for a' being Element of L' st a = a' holds
( a is_less_than X iff a' is_less_than X )
let a' be Element of L'; :: thesis: ( a = a' implies ( a is_less_than X iff a' is_less_than X ) )
assume A1: a = a' ; :: thesis: ( a is_less_than X iff a' is_less_than X )
thus ( a is_less_than X implies a' is_less_than X ) :: thesis: ( a' is_less_than X implies a is_less_than X )

proof

assume A2: a is_less_than X ; :: thesis: a' is_less_than X

now

let q' be Element of L'; :: thesis: ( q' in X implies a' [= q' )
the carrier of L' c= the carrier of L by NAT_LAT:def 16;
then reconsider q = q' as Element of L by TARSKI:def 3;
assume q' in X ; :: thesis: a' [= q'
then A3: a [= q by A2, LATTICE3:def 16;
a' "/\" q' = a "/\" q by A1, Th12
.= a' by A1, A3, LATTICES:21 ;
hence a' [= q' by LATTICES:21; :: thesis: verum

end;

hence a' is_less_than X by LATTICE3:def 16; :: thesis: verum

end;

thus ( a' is_less_than X implies a is_less_than X ) :: thesis: verum

proof

assume A4: a' is_less_than X ; :: thesis: a is_less_than X

now

let q be Element of L; :: thesis: ( q in X implies a [= q )
assume A5: q in X ; :: thesis: a [= q
then reconsider q' = q as Element of L' ;
A6: a' [= q' by A4, A5, LATTICE3:def 16;
a "/\" q = a' "/\" q' by A1, Th12
.= a by A1, A6, LATTICES:21 ;
hence a [= q by LATTICES:21; :: thesis: verum

end;

hence a is_less_than X by LATTICE3:def 16; :: thesis: verum

end;