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

( X is_less_than a iff X is_less_than a9 )

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

( X is_less_than a iff X is_less_than a9 )

let X be Subset of L9; :: thesis: for a being Element of L

for a9 being Element of L9 st a = a9 holds

( X is_less_than a iff X is_less_than a9 )

let a be Element of L; :: thesis: for a9 being Element of L9 st a = a9 holds

( X is_less_than a iff X is_less_than a9 )

let a9 be Element of L9; :: thesis: ( a = a9 implies ( X is_less_than a iff X is_less_than a9 ) )

assume A1: a = a9 ; :: thesis: ( X is_less_than a iff X is_less_than a9 )

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

for X being Subset of L9

for a being Element of L

for a9 being Element of L9 st a = a9 holds

( X is_less_than a iff X is_less_than a9 )

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

( X is_less_than a iff X is_less_than a9 )

let X be Subset of L9; :: thesis: for a being Element of L

for a9 being Element of L9 st a = a9 holds

( X is_less_than a iff X is_less_than a9 )

let a be Element of L; :: thesis: for a9 being Element of L9 st a = a9 holds

( X is_less_than a iff X is_less_than a9 )

let a9 be Element of L9; :: thesis: ( a = a9 implies ( X is_less_than a iff X is_less_than a9 ) )

assume A1: a = a9 ; :: thesis: ( X is_less_than a iff X is_less_than a9 )

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

proof

thus
( X is_less_than a9 implies X is_less_than a )
:: thesis: verum
assume A2:
X is_less_than a
; :: thesis: X is_less_than a9

end;now :: thesis: for q9 being Element of L9 st q9 in X holds

q9 [= a9

hence
X is_less_than a9
; :: thesis: verumq9 [= a9

let q9 be Element of L9; :: thesis: ( q9 in X implies q9 [= a9 )

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: q9 [= a9

then A3: q [= a by A2;

q9 "/\" a9 = q "/\" a by A1, Th11

.= q9 by A3, LATTICES:4 ;

hence q9 [= a9 by LATTICES:4; :: thesis: verum

end;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: q9 [= a9

then A3: q [= a by A2;

q9 "/\" a9 = q "/\" a by A1, Th11

.= q9 by A3, LATTICES:4 ;

hence q9 [= a9 by LATTICES:4; :: thesis: verum

proof

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

end;now :: thesis: for q being Element of L st q in X holds

q [= a

hence
X is_less_than a
; :: thesis: verumq [= a

let q be Element of L; :: thesis: ( q in X implies q [= a )

assume A5: q in X ; :: thesis: q [= a

then reconsider q9 = q as Element of L9 ;

A6: q9 [= a9 by A4, A5;

q "/\" a = q9 "/\" a9 by A1, Th11

.= q by A6, LATTICES:4 ;

hence q [= a by LATTICES:4; :: thesis: verum

end;assume A5: q in X ; :: thesis: q [= a

then reconsider q9 = q as Element of L9 ;

A6: q9 [= a9 by A4, A5;

q "/\" a = q9 "/\" a9 by A1, Th11

.= q by A6, LATTICES:4 ;

hence q [= a by LATTICES:4; :: thesis: verum