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

proof

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

now :: thesis: for q9 being Element of L9 st q9 in X holds
a9 [= q9

let q9 be Element of L9; :: thesis: ( q9 in X implies a9 [= q9 )
the carrier of L9 c= the carrier of L by NAT_LAT:def 12;
then reconsider q = q9 as Element of L ;
assume q9 in X ; :: thesis: a9 [= q9
then A3: a [= q by A2;
a9 "/\" q9 = a "/\" q by A1, Th11
.= a9 by A1, A3, LATTICES:4 ;
hence a9 [= q9 by LATTICES:4; :: thesis: verum

end;

hence a9 is_less_than X ; :: thesis: verum

end;

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

proof

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

now :: thesis: for q being Element of L st q in X holds
a [= q

let q be Element of L; :: thesis: ( q in X implies a [= q )
assume A5: q in X ; :: thesis: a [= q
then reconsider q9 = q as Element of L9 ;
A6: a9 [= q9 by A4, A5;
a "/\" q = a9 "/\" q9 by A1, Th11
.= a by A1, A6, LATTICES:4 ;
hence a [= q by LATTICES:4; :: thesis: verum

end;

hence a is_less_than X ; :: thesis: verum

end;