let S be non empty RelStr ; :: thesis: for T being non empty reflexive antisymmetric RelStr
for f, g being Element of (UPS (S,T)) holds
( f <= g iff for s being Element of S holds f . s <= g . s )
let T be non empty reflexive antisymmetric RelStr ; :: thesis: for f, g being Element of (UPS (S,T)) holds
( f <= g iff for s being Element of S holds f . s <= g . s )
let f, g be Element of (UPS (S,T)); :: thesis: ( f <= g iff for s being Element of S holds f . s <= g . s )
A1: UPS (S,T) is full SubRelStr of T |^ the carrier of S by Def4;
then reconsider a = f, b = g as Element of (T |^ the carrier of S) by YELLOW_0:58;
A2: ( f <= g iff a <= b ) by A1, YELLOW_0:59, YELLOW_0:60;
hence ( f <= g implies for s being Element of S holds f . s <= g . s ) by Th14; :: thesis: ( ( for s being Element of S holds f . s <= g . s ) implies f <= g )
assume for s being Element of S holds f . s <= g . s ; :: thesis: f <= g
hence f <= g by A2, Th14; :: thesis: verum