thus types A is lower :: thesis: types A is directed

proof

let x, y be Element of T; :: according to WAYBEL_0:def 19 :: thesis: ( not x in types A or not y <= x or y in types A )
assume A1: ( x in types A & y <= x ) ; :: thesis: y in types A

now

let a be adjective of T; :: thesis: ( a in A implies y in types a )
assume a in A ; :: thesis: y in types a
then x in types a by A1, Def13;
then ( a in adjs x & adjs x c= adjs y ) by A1, Th10, Th13;
hence y in types a by Th13; :: thesis: verum

end;

hence y in types A by Def13; :: thesis: verum

end;

let x, y be Element of T; :: according to WAYBEL_0:def 1 :: thesis: ( not x in types A or not y in types A or ex b₁ being Element of the carrier of T st
( b₁ in types A & x <= b₁ & y <= b₁ ) )
assume A2: ( x in types A & y in types A ) ; :: thesis: ex b₁ being Element of the carrier of T st
( b₁ in types A & x <= b₁ & y <= b₁ )

A3: now

let a be adjective of T; :: thesis: ( a in A implies x "\/" y in types a )
assume a in A ; :: thesis: x "\/" y in types a
then ( x in types a & y in types a ) by A2, Def13;
then ( a in adjs x & a in adjs y ) by Th13;
then a in (adjs x) /\ (adjs y) by XBOOLE_0:def 4;
then a in adjs (x "\/" y) by Def11;
hence x "\/" y in types a by Th13; :: thesis: verum

end;

take x "\/" y ; :: thesis: ( x "\/" y in types A & x <= x "\/" y & y <= x "\/" y )
thus ( x "\/" y in types A & x <= x "\/" y & y <= x "\/" y ) by A3, Def13, YELLOW_0:22; :: thesis: verum