let V, C be set ; :: thesis: for a, b being Element of (SubstPoset V,C) holds
( a <= b iff for x being set st x in a holds
ex y being set st
( y in b & y c= x ) )
let a, b be Element of (SubstPoset V,C); :: thesis: ( a <= b iff for x being set st x in a holds
ex y being set st
( y in b & y c= x ) )
reconsider a9 = a, b9 = b as Element of (SubstLatt V,C) ;
reconsider a1 = a, b1 = b as Element of SubstitutionSet V,C by SUBSTLAT:def 4;
A1: ( a9 % = a & b9 % = b ) ;

hereby :: thesis: ( ( for x being set st x in a holds
ex y being set st
( y in b & y c= x ) ) implies a <= b )

assume a <= b ; :: thesis: for x being set st x in a holds
ex y being set st
( y in b & y c= x )
then a9 [= b9 by A1, LATTICE3:7;
then a9 = a9 "/\" b9 by LATTICES:21
.= the L_meet of (SubstLatt V,C) . a9,b9 by LATTICES:def 2
.= mi (a1 ^ b1) by SUBSTLAT:def 4 ;
hence for x being set st x in a holds
ex y being set st
( y in b & y c= x ) by HEYTING2:8; :: thesis: verum

end;

assume for x being set st x in a holds
ex y being set st
( y in b & y c= x ) ; :: thesis: a <= b
then mi (a1 ^ b1) = a1 by HEYTING2:9;
then a9 = the L_meet of (SubstLatt V,C) . a9,b9 by SUBSTLAT:def 4
.= a9 "/\" b9 by LATTICES:def 2 ;
then a9 [= b9 by LATTICES:21;
hence a <= b by A1, LATTICE3:7; :: thesis: verum