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 ( x in types a & y <= x ) ; :: thesis: y in types a
then ( a in adjs x & adjs x c= adjs y ) by Th10, Th13;
hence y in types a by Th13; :: 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 ( 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₁ )
then ( a in adjs x & a in adjs y ) by Th13;
then a in (adjs x) /\ (adjs y) by XBOOLE_0:def 4;
then A1: a in adjs (x "\/" y) by Def11;
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 A1, Th13, YELLOW_0:22; :: thesis: verum