let n, m be Nat; :: thesis: ( n <= m implies InclPoset n is full SubRelStr of InclPoset m )
assume A1: n <= m ; :: thesis: InclPoset n is full SubRelStr of InclPoset m
A2: the carrier of (InclPoset m) = m by YELLOW_1:1;
A3: n c= m by A1, NAT_1:40;
then A4: the carrier of (InclPoset n) c= the carrier of (InclPoset m) by A2, YELLOW_1:1;
A5: the InternalRel of (InclPoset n) = RelIncl n by YELLOW_1:1;
A6: the InternalRel of (InclPoset m) = RelIncl m by YELLOW_1:1;
A7: RelIncl n c= RelIncl m

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in RelIncl n or x in RelIncl m )
assume x in RelIncl n ; :: thesis: x in RelIncl m
then x in (RelIncl m) |_2 n by A3, WELLORD2:8;
hence x in RelIncl m by XBOOLE_0:def 4; :: thesis: verum

end;

(RelIncl m) |_2 n = the InternalRel of (InclPoset n) by A3, A5, WELLORD2:8;
then the InternalRel of (InclPoset n) = the InternalRel of (InclPoset m) |_2 the carrier of (InclPoset n) by A6, YELLOW_1:1;
hence InclPoset n is full SubRelStr of InclPoset m by A4, A5, A6, A7, YELLOW_0:def 13, YELLOW_0:def 14; :: thesis: verum