let S be non empty SubRelStr of A; :: thesis: ( S is full implies S is connected )
assume A1: S is full ; :: thesis: S is connected
for x, y being Element of S holds
( x <= y or y <= x )
proof
let x, y be Element of S; :: thesis: ( x <= y or y <= x )
A2: the carrier of S c= the carrier of A by YELLOW_0:def 13;
reconsider b = y as Element of A by A2;
reconsider a = x as Element of A by A2;
( a <= b or b <= a ) by WAYBEL_0:def 29;
hence ( x <= y or y <= x ) by A1, YELLOW_0:60; :: thesis: verum
end;
hence S is connected by WAYBEL_0:def 29; :: thesis: verum